Book XIX · Chapter 3 · 2026-09-27 · Architecture
MATHEMATICS · FORMAL VERIFICATION
Elaborator, Macro, Kernel
Which program complained, and which one fixed it
When Lean refuses a proof, the complaint comes from one of a few programs in a pipeline, and each program has a different contract with you. Ullrich's dissertation draws the pipeline. This chapter sorts this corpus's own failures by the layer that raised them, and in almost every case the fix belonged to a different layer than the one that complained.
1 · The pipeline
Parser, macro expansion, elaborator, kernel
Ullrich's Fig. 3.1 (p.34) runs input through the parser, macro expansion and the elaborator, and then hands the result to the kernel. The core language output "is then checked by the kernel (Section 3.2), which is an independent component in order to minimize the Trusted Code Base" (p.34). CITED
The division of labour follows from that. Everything before the kernel may be clever, large and wrong. The kernel must be small and right. Ullrich says it plainly about tactics: "metaprograms are not part of Lean's Trusted Code Base — after execution, their output is checked by the kernel just as if we had written down the output manually" (p.15). CITED
The consequence for a reader
A tactic cannot make a false theorem true. It can only fail to produce a term, or produce one the kernel rejects. What a reader must trust is the kernel, plus whatever extra axioms a proof admits, and #print axioms reports those.
2 · Three facts from the source
- "The Lean kernel does not accept any kind of recursion in regular definitions; recursion is instead transformed by the frontend into applications of recursors" (p.15). A recursive definition you write is not the term the kernel sees. CITED
- "The kernel type checker does not use a metavariable context and will reject remaining metavariables" (p.19). A hole the elaborator could not fill never reaches the kernel as a hole. CITED
- Natural-number literals are computed by an arbitrary-precision library, "which therefore becomes part of the Trusted Code Base" (p.36). Even the small kernel trusts some fast arithmetic. CITED
3 · This corpus, by layer
Who complained, and who fixed it
| incident | raised by | fixed in |
|---|
| decide on addc in Book XII ch2 would not evaluate | kernel evaluation (the Decidable instance did not reduce) | elaborator: rw [addc_correct]; simp [val], i.e. rewriting with equation lemmas instead of computing |
| native_decide in CollatzDescent.lean | nobody: it succeeds | the gate: it adds the axiom Lean.ofReduceBool, which puts the compiler inside the trusted base |
| sorry in four files | elaborator (a warning, not an error) | the gate: sorryAx appears in #print axioms |
| "#print axioms counted as a failure" (FixedPointConclusion, 2026-09-25) | our own script | the gate now enumerates the permitted three axioms; it no longer greps for forbidden words |
The corpus carries 709 #print axioms lines in 73 of its 110 files. tools/leancheck.sh --audit defers its verdict to tools/axiom_gate.py, which accepts exactly propext, Classical.choice and Quot.sound. The script's own header records why a forbidden-word list fails: Lean.ofReduceBool "leaks straight through the name native_decide". COMPUTED
The pattern
In each row the fix sits one layer away from where the complaint was raised. The kernel stalled and the elaborator fixed it; the elaborator was silent and the gate caught it. That pattern is our reading, not Ullrich's claim. MODEL
Not establishedWhy decide stalled on addc was not diagnosed beyond the layer that reported it. The definition's three-way match, with a carry that changes on every call, is the likely suspect. OPEN The thesis describes Lean 4 as of 2023; the toolchain here is v4.32.0.
See also WP-73 on why a forbidden list is the wrong shape for a gate, and Chapter 4 for the layer below all of these: whether the named file exists at all.
- S. Ullrich, An Extensible Theorem Proving Frontend, dissertation, KIT, 2023 (255 pp). Printed page = PDF page − 12, checked at pp.34 and 36. Hash in docs/floor-texts.tsv.