A two-day evaluation of Lean 4's classical automation cascade on a small curated math corpus, with an LLM-hint stage probing whether residuals close after retrieval. The methodology stack is more reusable than the empirical numbers; the corpus is too small to settle the headline question.
Each of 100 stratified problems (60 Mathlib, 30 miniF2F-v2c, 10 miniCTX) runs through 15 probes spanning six cascade stages: rfl/decide/native_decide, simp, ring, linarith/omega, grind (7 variants), aesop. Closed proofs re-elaborate in a fresh Lean process under a strict axiom rule (no sorry, no non-foundational axioms). Cascade residuals get an LLM-hint stage: Claude Opus 4.7, Gemini 3 Pro, and GPT-5 each propose three Mathlib lemma names. Verified hints (name exists, type matches) get added to scope and the cascade re-runs.
20 of the 100 problems are held out and frozen until the end of the run, so the cascade and the LLM-hint stage are tuned only on the remaining 80. The 80-problem set is referred to as the dev set below; the held-out 20 became 19 after MC-091 was excluded for an unrelated Lean-4.29.1 elaboration issue.
Of the 20 dev problems closed by anything, no problem closes uniquely at stages 1, 2, 3, or 4. Only grind (3 unique closes) and aesop (4) close problems nothing else does. The held-out 6 closes show the same pattern: only aesop earns unique closes (2). The data are consistent with the simpler cascade by grind <;> aesop. The unique-close metric measures stages in isolation, so call this a hypothesis well-supported by the data, not a directly tested cascade. Lean 4.29.1 specific. Mathlib SHA 5e932f97... specific.
Pooled rescue rate across the three models: 15 of 57 dev residuals (26.3%, Wilson 95% CI 16.6%-39.0%). Held-out: 1 of 13 (7.7%, CI 1.4%-33.3%).
A post-hoc audit changes the reading sharply. Of those 15 dev rescues, 13 used the upstream Mathlib name of the problem itself (e.g. GPT-5 suggesting MeasureTheory.tendsto_setToFun_approxOn_of_measurable_of_range_subset for ML-MEA-031, the canonical name of that problem's source). The model named the lemma whose statement it was just shown. That is recall, not retrieval of a different useful lemma. Subtracting recall, the corrected dev "true retrieval" rate is 2 of 57, or 3.5% (CI 1.0%-11.9%). Decisively reasoning-dominated under the pre-registered decision rule. Held-out true retrieval is 0 of 13.
The audit caveat was post-hoc; the dev "mixed" verdict survived only because of those 13 recall rows. The pre-registered question, asked honestly, gets a much weaker answer than the headline.
GPT-5's Layer-1 hallucination rate (75%, CI 68%-81%) is significantly higher than Claude (44%) or Gemini (43%). Despite this, GPT-5 also rescued more dev residuals than the other two; see SURPRISES.md 2026-05-14. The relationship is correlational across n=3 models. We cannot claim hallucinations help; verification filters all hallucinations before re-cascade. The plausible reading is that the same generative behavior produces both the noisy outputs and the operative ones, and verification makes the noise tractable.
A research paper. N=100 dev / N=19 held-out yields confidence intervals too wide to settle the retrieval-vs-reasoning question. The corpus is curated, not crawled. The single Lean version pins everything to one moment in 2026. Proof-finding capability is not measured against frontier prover systems (HILBERT, DeepSeek-Prover-V2, Aristotle); the comparison would require running them on this corpus, which was not done. To answer the headline with tight CIs the corpus would need roughly 5x the size.
The reusable contribution is the methodology stack: pre-registration with inline CHANGELOG, kernel-replay verification, strict-vs-lenient closure with native_decide axiom auditing, run-to-run determinism check, three-model cross-provider hint stage with explicit upstream-recall accounting, audit gates with sample-seed pre-commitment.
Defensible:
- On this corpus, stages 1 to 4 contribute zero unique closes on both dev and held-out.
- Determinism: 0 outcome diffs and 0 verdict diffs across two cascade passes (1200 probe rows each); 0 grind verdict flips across 5 reruns per dev problem in either pass.
- Cross-provider design is methodologically load-bearing: a single-model headline would have placed the verdict anywhere in the per-model dev range (1.7% to 19.3%).
- The methodology pipeline as a reusable template.
Uncertain or unsupported:
- The pre-registered headline verdict. Dev says mixed, dev recall-corrected says reasoning-dominated, held-out says reasoning-dominated, CIs overlap, N is too small.
- Per-model rescue ranking. Claude vs GPT-5 CIs overlap.
- Anything generalizing beyond Lean 4.29.1 + the pinned Mathlib commit.
Lean 4.29.1 via elan. Mathlib pinned in manifest.json. Python 3.11+. API keys in ~/.lean-cascade-eval-keys.
make full
python3 scripts/gen_figures.pyCost: ~$5 LLM API. ~6 hours CPU.
PREREG.md pre-registration with inline CHANGELOG (live spec)
STATS.md headline numbers, each with a reproducible query
manifest.json Lean version, Mathlib SHA, model IDs, seeds, prompt hash
canaries/ trivial must-close problems
corpus/ 100 problems with per-problem statement + header + meta
audit/ manual-audit samples and logs
scripts/ runner, replay, hint pipeline, analysis
results/ per-run JSONL logs
docs/ figures and supporting material
notes/ SURPRISES.md (running log of what surprised the runner)
MIT, see LICENSE.
mathnet-eval-harness: same author, LLM-on-math eval, reused the harness pattern.