A machine-checked proof that Lean's typechecker implements its declarative type theory
Difficulty 48: the declarative theory and parts of the checker are already formalized in Lean4Lean, and the analogous verified checker for Coq's core calculus exists (MetaCoq), so the path is visible; what remains is a large effort on nested and mutual inductives, quotients and reduction rules against a kernel that keeps changing. That places it above the FLT integration (38) and below research problems with no visible route (55 and up). Application value 32: it removes the last unverified component under every Lean result, above the FLT library (29) because it covers all machine-checked mathematics. Leverage 42: all Lean results rest on the kernel, but independent kernels (nanoda re-checked the 2026 FLT certificate) already reduce the practical risk, so it stays below subfield-reshaping problems such as diagonal Ramsey (46).
The problem
Prove, in Lean itself, that the program that checks Lean proofs follows the rules it is supposed to.
- 1One small program decides every proof
- 2Write a second checker in Lean
- 3Prove it follows the written rules
- 4Re-check it with a third, independent checker
The question in plain terms. Lean's kernel is the small program that says yes or no to every proof (see the kernel entry). Everything proved in Lean is only as trustworthy as that program. This problem asks for a mathematical proof, itself checked by computer, that a kernel does exactly what the rules of Lean's logic say it should.
Two descriptions of the same thing. The rules of the logic can be written on paper as inference rules: "if has type and has type , then has type ", and so on for every feature. Call this the system: it says which judgements are valid, not how to decide them. The kernel is an : given a term and a type, it runs and answers yes or no. The task is to prove two theorems linking them:
Start with Lean 4 kernel and dependent type theory. No foundations are linked to it yet; if you know what a reader needs first, say so in the discussion below so a maintainer can link it.
State of the art
Carneiro's Lean4Lean (arXiv:2403.14064, 2024; version 3, 14 September 2025, submitted to CPP 2026) is a complete external typechecker for Lean 4 written in Lean. It runs about 20% to 50% slower and checks all of Mathlib. The paper formalizes Lean's type theory abstractly, proves metatheoretic properties, and proves correctness of parts of the kernel; verifying the whole checker is stated as ongoing. The project has found and fixed a soundness bug. A second independent kernel, nanoda (written in Rust), is supported by Lean's Comparator tooling, and it accepted an export of the 13-million-line Fermat's Last Theorem development in September 2026 (repository README), so independent re-checking already works at scale; what is missing is a proof that any checker matches the declarative rules. Comparator was merged into Lean core as lake comparator from release v4.35.0 per its README.
Realistic applications
Every machine-checked result in Lean, including AI-produced certificates such as multi-million-line proofs, bottoms out in kernel trust. A verified checker turns the remaining soft spot (a bug in the C++ kernel) into a hard theorem and makes it safe to accept machine-produced proofs without human review of the proof text.
What counts as solved
A Lean development, checked by a kernel independent of the one being verified, containing the declarative typing relation, a typechecker and a proof that it is sound and complete for the full feature set, with a build that shows the verified checker accepts all of Mathlib; and an explicit list of any remaining trust assumptions (the declarative rules and the kernel that checks the development).
How it gets verified
Lean proofA formal proof checked by Lean 4 / Mathlib.
The result is a Lean development, so the judge is a Lean kernel other than the one whose behaviour is verified: export the development with lean4export and recheck it with an independent kernel (nanoda, or Lean4Lean once its own correctness is trusted), and require only the three standard axioms. The statement is not yet fixed in Lean source in a corpus; it should be written as a pair of theorems in the style of digama0/lean4lean: soundness (every term accepted by the checker is derivable in the declarative system) and completeness (every declaratively derivable judgment is accepted). Mathlib does not contain this; it is a separate project that depends on the Lean core data structures. The paper's claim about which parts are verified should be checked against the repository at a pinned commit before this task is declared open or closed.
Claims under verification
+ add a claimNo claimed results on the Verification board for this problem yet.
Where the work is
The type theory and parts of the checker are formalized; the rest is a large verification engineering effort with some theory for nested inductives and quotients.
Bottlenecks
ranked by votes- #1EngineeringSize and drift of the kernel
The checker has many reduction rules and special cases and Lean changes releases frequently; proofs must track the kernel.
Community grades
Sign in to add your own grade.
Connected problems
No connections yet.