Kernel status
loading…
repo—
commit—
toolchain—
last lake build—
Canonical numbers (live)
—
declarations
—
axioms (raw)
—
axioms (unique)
—
sorries (raw)
—
sorries (non-comment)
lake build (on demand)
idle
Press “Run lake build” to kernel-check the whole library live. (First run on a cold box downloads the Mathlib cache and can take minutes; if disk/cache is unavailable the failure is shown here verbatim.)
Theorem table (PROVEN / AXIOM / SORRY)
PROVEN —
AXIOM —
SORRY —
| status | kind | name | file:line |
|---|---|---|---|
| loading… | |||
Λ-receipt verifier playground
POST a receipt
{"axes":[...], "lambda":…}. The kernel recomputes Λ = (∏xᵢ)^(1/k) and names the confirming theorem.—
10 golden reference vectors
—
—
API
GET /api/lean/healthz ·
GET /api/lean/numbers ·
GET /api/lean/theorems ·
POST /api/lean/verify ·
GET /api/lean/build (SSE) ·
GET /api/lean/vectors ·
POST /api/lean/vectors/exercise