01 · What it is
What Lean is, and why it matters
Lean 4 is a proof assistant, software that checks mathematical proofs with machine precision. You write a theorem in Lean's language, and the computer either accepts the proof as correct or tells you exactly where it breaks. Its community library, mathlib, is an ongoing effort to digitize as much pure mathematics as possible in one large cohesive library: over 210,000 theorems and 100,000 definitions as of May 2025. Beyond mathematics, Lean matters to hardware and software verification (proving a chip or a protocol behaves as specified) and, increasingly, to AI: the 2026 proof-search literature builds agents that try thousands of tactic steps against proof states, and Lean is the environment they run in. Lean 4 itself (released 2021) was already a reimplementation — a rebuild of the older Lean as a general-purpose programming language as well as a prover.
A prover toolchain has one decisive property: trust. The whole edifice rests on a small checking kernel, the component that says "yes, this proof is valid," which must be simple enough to audit and correct enough to bet theorems on. Everything else (the elaborator that turns your syntax into proof terms, the compiler, the build system, the editor integration) exists to serve that trust. That is the component this project chose to re-derive first.
02 · Why build it
Why rewrite it in Rust?
The maintainer's stated case, in the project's docs: the Reference (the official Lean 4 implementation) carries costs this project names explicitly: a C++ trusted computing base, a stage0 bootstrap, file-granular builds, an import tax of roughly 60 seconds per worker, and schedule-sensitive asynchronous elaboration. The agent-era argument is the sharpest: 2026 proof-search papers hand-roll prover harnesses per paper to run thousands of tactic applications against forked proof states; a native Rust toolchain with O(1) proof-state snapshots and agent surfaces (a serve-mcp command, a goals command) would be the substrate those agents actually want.
The counter-argument, which the project's own bear-case analysis does not flinch from: a prover toolchain is a compatibility product, and compatibility is won by running the corpus. The Reference is the only implementation that elaborates all of mathlib, runs its tactics, loads its .olean files, and serves editors; this project's compatibility is staged per surface with most surfaces at the earliest level. And the Reference improves monthly. Every upstream release is a ratchet the project runs alone, doubling its conformance debt with each missed epoch. One maintainer, a stated no-outside-contributions policy, and a license rider that bars the AI labs (the named customers of the agent-era bets) from even benchmarking the code make the climb structurally lonely.
03 · What was built
What the project actually built
The scale is startling: 731,657 lines of Rust across 32 crates, zero external crates.io dependencies anywhere in the lockfile. The closed dependency universe is not marketing. What demonstrably exists: a bounded vertical slice in which one source file traverses a Pratt parser, a bounded elaborator (Nat/Bool/String definitions, #eval, #check), a dual-checking kernel (the certified small-step evaluator K1 plus an independent checker crate that re-verifies independently), then a compiler to a register VM that executes. The kernel compiles under forbid(unsafe_code) with zero unsafe blocks. That is the verified core.
But the project's most distinctive asset is its specification handcuffed to the enemy:
- Kernel rules anchored to upstream source lines.
KERNEL_CONTRACT.md binds every rule of the judgment spec to the exact upstream file and line: anchor: vendor/lean4-src/src/kernel/type_checker.cpp:289 … expect="infer_type_core". A conformance test fails CI (continuous integration: automated checks that run on every change) if the token on that line ever changes. The spec machine-detects when upstream moves underneath it. - A CI-enforced unsafe-site ledger. The one place the "100% safe Rust" tagline breaks, the three boundary crates (foreign-function ABI, memory regions, a JIT stub) containing project-authored unsafe, is documented in a 697-row ledger with a bidirectional census that passed CI at the pin (the commit the assessment was pinned to). The breach is fenced, counted, and gated.
- A claim matrix with a tense note. The README opens by confessing it is written "in the present tense, as if the entire design… is fully realized," describing the 1.0 target state rather than the pin, and the implementation-status file runs a five-tier evidence vocabulary (landed / model-verified / artifact-bound / observed / target) where "landed" does not mean verified.
Evidence · CI status
What the project’s own CI said at the pin
- ✕CI is red at the pin: the main quality gate failed 11 of 30 steps, including the gate self-test and six end-to-end smokes.
The uncomfortable findings
Uncomfortable finding
The pattern of what passed is telling: the unsafe census, the extern censuses, the snapshot smokes. The gates that enforce honesty pass while the gates that assert capability fail. K2 does not exist: the accelerated kernel engine named on the architecture badges is explicitly disclaimed in the code ("does not claim K2 or NbE exists"). The ≤12 KLOC kernel badge is already spent: the kernel library alone is 17,051 lines. Performance is an honest zero: the README states verbatim "0 bench targets, 0 committed baselines and 0 flame artifacts," and every gate-table number is TARGETED. The "independent" checker is 68,243 lines, several times the kernel it checks, written by the same single author, so "independent" means implementation-diverse, not institutionally independent. And the flagship FrankenSuite integrations named in doctrine (the asupersync runtime, the frankensqlite store) are pinned in a lockfile and appear in zero crate manifests: unwired foundations.
04 · Where it stands
Where it stands
In our program's terms: TRL 4, NODUS ring Explore. In plain English: bounded slices execute in the lab; nothing has run the corpus, nothing has shipped, no independent party has validated any of it. Real technical substance (a real kernel, a real VM, real methodology), but zero release artifacts and red CI.
Technology readiness
TRL 4 on a 1-to-9 scale.
NODUS ring
MonitorExplorePilotInvest
The program’s adoption ring for this project.
Verdict key
- NODUS ring
- Explore: The default for substantive-but-unproven work.
- TRL
- Technology Readiness Level, a 1-to-9 scale of how proven a technology is. This brief rates the project at TRL 4.
- CI
- Continuous integration: the project’s automated checks, run on every change.
- The pin
- The exact commit the assessment was pinned to. “At the pin” means as of that commit.
Evidence tiers
- Tier 1 · Verified — Confirmed by direct inspection of a fresh clone, an API response, or a live page read by the analyst.
- Tier 2 · CI-observed — Observed executing on live CI pages. Attests the suite runs, not that it is green, unless pass/fail is legible.
- Tier 3 · Maintainer claim — Asserted in README or docs by the maintainer; not independently executed or reproduced.
- Tier 4 · External — Independent sources: APIs, papers, press, third-party benchmarks. Absence of coverage is reported as a finding.
- Tier 5 · Inference — The analyst’s judgment. Always labeled; never presented as fact.
What this verdict rests on. Tier labels are the assessment packet’s own annotations.
- Tier 1 · Verified: 7,140
#[test] annotations counted as a declared inventory; the README’s note on tense is verified README text. - Tier 2 · CI-observed: CI gate fails at the pin, from step-level conclusions only.
- Tier: unassessed in packet: The exact failing assertions behind the CI failure were not established.
- Tier 3 · Maintainer claim: No test was executed; the bounded slices execute only in the maintainer’s lab.
- Tier 4 · External: No releases, no tags; star counts from a live API read.
- Tier 5 · Inference: The Explore ring at TRL 4.
Should you use it?
No.
If you need to formalize mathematics today, the Reference is the only toolchain that runs your project.
Should you learn from it?
Yes — and specifically from the anchored spec.
The anchor:/expect= mechanism generalizes to any clean-room project: bind your specification to the upstream source lines it re-derives and let CI scream when the enemy moves. The unsafe-site ledger ports anywhere too.
What would change the verdict, in order
- a green main CI gate at a pin, a tagged release or installable toolchain artifact, K2 landing (making the badge true), corpus-scale differential parity against the Reference on mathlib, and, as the structural fix, any softening of the no-contributions policy or the license rider
- Until then, the Reference wins every adoption criterion except auditability, and this project's auditability is currently its only export
source
05 · What it teaches
What this teaches about building with agents
Here is the exportable insight, and it applies far beyond theorem provers.
Every clean-room rewrite eventually lies to itself about the thing it is cloning. The drift is not usually malice — it is entropy: upstream ships monthly, your spec was written in spring, and by autumn you are checking against a memory. This project's answer is to handcuff the spec to the enemy's source code: every rule carries an anchor naming the exact upstream file and line plus an expect= token, and a CI test fails when the token on that line changes. The specification cannot go stale quietly, because staleness is a build failure.
The deeper point is about what you anchor to. Most projects anchor to their own roadmap, which moves when you move it. Anchoring to the thing you are re-deriving externalizes the tripwire: the ratchet you fear — upstream moving without you — becomes the signal you instrument. The maintainer here even built the social layer of the same discipline: the README's tense note (target-state prose, admitted as such) and the five-tier evidence vocabulary. source For anyone building with agents, which will happily re-derive a stale snapshot and report it as current, the lesson is: point your drift-detection at the outside world, not at yourself, and make drift fail the build. The projects that do this will still go stale. They just won't get to pretend they didn't.