# Lean4Lean: Verifying a Typechecker for Lean, in Lean

arXiv: https://arxiv.org/abs/2403.14064 · HTML: https://mlsanity.com/paper/2403.14064/

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 21 Mar 2024.

## Built on by (most cited first, 8 of 8)

- [Physics Supernova: AI Agent Matches Elite Gold Medalists at IPhO 2025](https://mlsanity.com/paper/2509.01659/) (2025)
- [Faithful Logic Embeddings in HOL -- Deep and Shallow](https://mlsanity.com/paper/2502.19311/) (2025)
- [Proof-Carrying Certificates for LLM Pipelines: A Trust-Boundary Architecture](https://mlsanity.com/paper/2605.16407/) (2026)
- [KELPS: A Framework for Verified Multi-Language Autoformalization via Semantic-Syntactic Alignment](https://mlsanity.com/paper/2507.08665/) (2025)
- [Formally Verified Patent Analysis via Dependent Type Theory: Machine-Checkable Certificates from a Hybrid AI + Lean 4 Pipeline](https://mlsanity.com/paper/2604.18882/) (2026)
- [LLMs Can See the Smoke but not the Fire: Evaluating Abductive Reasoning with Elenchos](https://mlsanity.com/paper/2607.12733/) (2026)
- [LeanCSP: A Framework for Certifying Constraint Reformulation and Solving in Lean](https://mlsanity.com/paper/2607.28459/) (2026)
- [The Future of AI-assisted Physics: Discovering, Verifying and Organizing Results via Formalization](https://mlsanity.com/paper/2610.14059/) (2026)

## Abstract (arXiv)

In this paper we present a new "external checker" for the Lean theorem prover, written in Lean itself. This is the first complete typechecker for Lean 4 other than the reference implementation in C++ used by Lean itself, and our new checker is competitive with the original, running between 20% and 50% slower and usable to verify all of Lean's mathlib library, forming an additional step in Lean's aim to self-host the full elaborator and compiler. Moreover, because the checker is written in a language which admits formal verification, it is possible to state and prove properties about the kernel itself, and we report on progress to formalize the Lean type theory abstractly and prove some theorems about it. Finally, we combine these to get a proof of correctness of parts of the kernel. We plan to use this project to help justify any future changes to the kernel and type theory and ensure unsoundness does not sneak in through either the abstract theory or implementation bugs. The verification is already paying off, as one soundness bug has been spotted and fixed as a result of this work.