Book XIX · Chapter 2 · 2026-09-27 · Census
MATHEMATICS · FORMAL VERIFICATION
The Idioms AXLE Reinvented
Which verbs a proof opens with, here and in the textbook
A tactic is the verb of a Lean proof. Count which verbs open each line, here and in the book Lean's own authors wrote for newcomers, and the two vocabularies overlap less than you might expect. The corpus has its own dialect, and most of it developed without anyone reading the textbook.
1 · The census
2,482 lines against 1,329
The script reads the 110 tracked .lean files in this repository, with comments stripped. It also reads the code in Avigad & Massot, Mathematics in Lean, v4.19.0 (214 pp). Then it counts every line that opens with a tactic name. COMPUTED
| tactic | corpus | share | MIL | share |
|---|
| have | 612 | 24.7% | 125 | 9.4% |
| rw | 355 | 14.3% | 145 | 10.9% |
| simp | 254 | 10.2% | 64 | 4.8% |
| unfold | 135 | 5.4% | 0 | 0.0% |
| nlinarith | 65 | 2.6% | 0 | 0.0% |
| omega | 52 | 2.1% | 2 | 0.2% |
| refine | 76 | 3.1% | 2 | 0.2% |
| apply | 21 | 0.8% | 87 | 6.5% |
| rfl | 1 | 0.0% | 62 | 4.7% |
| use | 1 | 0.0% | 58 | 4.4% |
| ext | 11 | 0.4% | 41 | 3.1% |
| sorry | 5 | 0.2% | 268 | 20.2% |
Three rows stand out.
- have opens a quarter of the corpus's lines. The corpus proves by stating intermediate facts and then discharging them.
- unfold appears 135 times in the corpus and never in MIL. MIL rewrites with a definition's lemma instead (rw [f], simp [f]).
- rfl and use, the two smallest closing moves in MIL, appear exactly once each in the corpus.
2 · The gaps
What each side never says
MIL opens at least five lines with contrapose and convert; the corpus never does. The corpus opens at least five lines with funext, nlinarith, push_cast, subst and unfold; MIL never does. COMPUTED
Decision procedures (norm_num, linarith, nlinarith, omega, decide, positivity, simp) open 21.3% of the corpus's lines and 7.4% of MIL's. A decision procedure answers a question without showing its reasoning. That is legitimate, and in Lean the answer is still kernel-checked. But it means the corpus's proofs carry the reader less far than MIL's do. COMPUTED
The idioms, reinvented
The corpus's unfold f; simp; nlinarith is a local reinvention of MIL's simp [f]; nlinarith, and MIL Ch. 2 teaches that pattern. The long have ladders do by hand what MIL's calc blocks (Ch. 2) lay out as a readable chain. The corpus uses calc only 20 times. MODEL
3 · The placeholders
sorry: 268 in the textbook, 5 here
MIL opens 268 lines with sorry, 20.2% of its code. These are the reader's exercises; each sorry is a blank for the reader to fill in. The corpus's five sit in four files:
- MagneticLattice.lean, under the default Orthogenesis target, declared in the file's own header;
- GenerativeWeave.lean, declared at the line;
- CollatzDescent.lean, which no lean_lib declares. It is also the only file with native_decide in live code;
- a deposit moved to docs/ml-evidence.
The same word does different jobs in the two sources. Chapter 1 covers what sorry admits. Chapter 3 covers which layer sees it. COMPUTED
What this chapter does not showA difference in shares is not a defect. MIL is a teaching text and this corpus is research code. The census counts verbs; it does not judge proofs. OPEN A proof-by-proof reading against MIL's chapter structure remains to be done.
- Avigad & Massot, Mathematics in Lean, v4.19.0 (214 pp). Held; hash in docs/floor-texts.tsv.