Trust model
This site presents formal mathematics. Some of what it shows you was established by a machine and some of it was asserted by a person, and the two look alike on the page. This is the separation.
What is machine-checked here
Everything in this table is a property of the build that produced the page you are reading. Nothing here is copied from a metadata file; where a check did not run, the row says so rather than being omitted.
| Check | This build | What it does not cover |
|---|---|---|
| Kernel type-checking | every declaration | Every Lean declaration presented here was accepted by the Lean 4.32.0 kernel during the build that produced this site. That is a check of the proofs, not of whether the statements say what you want. |
| Axiom audit | 196 clean | Lean.collectAxioms over 196 declarations: no sorryAx anywhere in any transitive closure, and no axiom beyond propext, Classical.choice, and Quot.sound. This subsumes transitive sorry detection — a theorem invoking a sorried lemma is caught even though its own body is clean. |
| Dependency-graph structure | acyclic, connected | The authored uses graph (45 nodes, 105 edges) was gated before this site was written: no dependency cycle, no unresolvable uses label. The *edges themselves* are author-asserted — see below. |
| Independent statement comparator | 1 theorem | A CI run using comparator 07bc4ea40f2266dcb861820a2ec1fa3244ed307f reported that the solution proves exactly the named challenge statement(s). This page reads that run's artifact back; it does not re-run the check. Scope is the named theorems only — everything else here is built and audited but not comparator-certified. |
| Mathematical notation (KaTeX) | enabled | Every inline and display formula was parsed by KaTeX at build time. This checks that the notation renders, not that it is mathematically apt. |
What is not machine-checked
The informal ↔ formal correspondence
This is the important one. Every node on this site places an informal statement beside a Lean declaration, and nothing anywhere in this stack checks that the two say the same thing. The side-by-side layout is an affordance for human audit — it puts the prose and the code where you can compare them — not a verification of their agreement. The same applies with more force to informal proofs: a :::proof block is free prose with no relation to the Lean proof term beside it.
If the Lean statement is a faithful rendering of the informal one, then the machine checks above tell you the theorem is proved. If it is not, they tell you nothing you care about. Reading the formal statement is the step that cannot be delegated.
Authored dependency edges
The dependency graph's edges are declared by the author with uses, not derived from the Lean terms. The build gates their structure (no cycles, no dangling labels) and compares them against the constants each declaration actually mentions, reporting divergence as a build warning — but an edge that exists only in the author's mind, or a real dependency the author did not draw, is a presentation defect the gates do not reject.
This build compared 45 node(s) against their Lean terms: 0 dependency edge(s) present in the code are not drawn in the graph, and 19 drawn edge(s) do not appear in the code (informal-level edges — a mathematical dependency the Lean proof reaches by another route).
How the Lean code on this page was rendered
Code blocks are produced by different pipelines, and they do not carry the same evidence. Each block is marked in its top-right corner:
| ⟲ | Re-elaborated from source | The declaration was elaborated again from the project's source text during the site build, so its tokens carry checked semantic information and its layout is exactly what the author wrote. |
| ≈ | Signature-only, or syntactic | Either the statement alone was re-elaborated (the proof was not re-run), or the text was parsed and coloured without elaboration. Token meanings are not checked. |
| ⌁ | Pretty-printed or raw | Rendered from the compiled declaration rather than the source file, or shown as plain text. Layout, notation, and implicit arguments may differ from the file you would read on GitHub. |
| ! | Source newer than the compiled build | The source file changed after the artifact the status was read from was compiled, so the displayed text and the reported status may disagree. |
A downgrade between tiers happens silently — a re-elaboration can exceed its time budget, or reference names that are not in scope outside their module. Marking the tier is what makes that visible.
Source links
"View source" links point at the commit the site was built from. They are constructed from the local git checkout, so if that checkout had uncommitted changes the link resolves to a commit that is not quite what was built; the build stamp marks such a build as dirty.
What you are trusting
The checks above are only as good as the things that performed them. Concretely, this site asks you to trust:
- The Lean kernel — version 4.32.0 — the program that accepted every proof here. See the next section on why that is not a closed question.
- Mathlib — at revision 81a5d257c8e410db227a6665ed08f64fea08e997, together with everything Mathlib itself depends on.
- The statement comparator — at commit 07bc4ea40f2266dcb861820a2ec1fa3244ed307f, and the GitHub Actions runner that executed it.
- nanoda — at revision f58f2f6d535e189a40fcb02ede8eb95f97a92d37, as the independent kernel.
- landrun — at revision 5ed4a3db3a4ad930d577215c6b9abaa19df7f99f, as the sandbox confining the solution during the replay.
- GitHub Actions — as the environment the verification ran in, and its logs as an honest record of what happened there.
- GitHub Pages — as the host serving these files unmodified.
Why independent verification — and what it does not settle
A proof accepted by the Lean kernel is accepted by one program. If that program has a soundness bug, everything it accepted inherits it. Re-checking the same proof with a second, independently written kernel is the standard defence: two implementations are unlikely to share a bug.
That defence is weaker than it sounds, and 2026 showed exactly how. A kernel soundness bug (Lean issue #14576) was found by way of an AI-assisted "disproof" of the Collatz conjecture that the kernel accepted. The same artifact was replayed against nanoda, an independent reimplementation — and nanoda accepted it too, not because the two share a design, but because the nanoda build being used was a week old and had its own, separate bug. Two independent checkers agreed, and both were wrong.
The lesson is that independence and currency are different properties, and you need both. A second kernel pinned to a revision from before a soundness fix is a second opinion from the past.
Verifier currency
Pinning a verifier by revision and keeping a verifier current are in tension. A pinned verifier gives a reproducible result: anyone can re-run exactly what CI ran. A current verifier gives a result that reflects every soundness fix known today. A single run cannot do both.
This project pins its independent kernel to nanoda f58f2f6d535e189a40fcb02ede8eb95f97a92d37. That pin makes the verification reproducible; it does not make it current.
The policy this project follows is to pin for reproducibility and to re-verify against current tooling on a schedule, reporting both. The scheduled re-verification is not yet implemented — the verdict shown on this site is a pinned one only, and nothing here re-checks it against today's kernels. This is tracked as future work rather than presented as done.
Known gap: no scheduled re-verification job, and no binding between the displayed verdict and a specific CI run beyond the recorded URL. Both are on the project's roadmap.
How this was produced
This project's formalization.yaml records that parts of the Lean development were produced with automated assistance:
- agent (Claude Code) — models: claude-fable-5
Automated or not, every declaration went through the same kernel and the same audit as the rest of the site. Automation changes who wrote the proof, not what checked it.