Leaderboard
Verified proof rate by configuration
Share of theorems for which the configuration produced a proof the certifier accepted, with a 95% Wilson interval. The same model and the same theorems throughout; configurations differ only in which parts of the loop are on.
| Configuration | Verified | Rate, 95% CI | ≤1 call | ≤2 | ≤4 | Median calls | Cost / verified |
|---|---|---|---|---|---|---|---|
| Template (no LLM) A fixed list of automation tactics (simp, omega, linarith, nlinarith, positivity, aesop, grind, exact?, …) tried in order. No model. | 46/174 | 26.4% | 26% | 26% | 26% | 0 | $0.00000 |
| Full (plan + retrieval + repair) A planning call (informal sketch plus a Lean `have` skeleton that Lean type-checks), then retrieval plus repair. | 13/174 | 7.5% | 0% | 4% | 7% | 2 | $0.026 |
| Full − skeleton The full agent with an informal plan only, no Lean skeleton. | 13/174 | 7.5% | 0% | 5% | 7% | 2 | $0.019 |
| BM25 retrieval + repair Retrieval + repair, with BM25 retrieval only. | 13/174 | 7.5% | 3% | 5% | 7% | 2 | $0.015 |
| Repair (paraphrased prompt) Repair with a paraphrased prompt (prompt-sensitivity check). | 12/174 | 6.9% | 3% | 6% | 7% | 2 | $0.011 |
| Full − memory The full agent, but each repair round shows only the latest attempt. | 11/174 | 6.3% | 0% | 4% | 6% | 2 | $0.028 |
| Repair One draft, then up to three rounds in which the model sees Lean's exact error output. | 11/174 | 6.3% | 1% | 5% | 6% | 2 | $0.015 |
| Full − compiler feedback The full agent, but a failed round only says the proof failed; Lean's output is withheld. | 10/174 | 5.7% | 0% | 4% | 6% | 2 | $0.031 |
| Full − retrieval The full agent without retrieved lemmas. | 9/174 | 5.2% | 0% | 5% | 5% | 2 | $0.030 |
| Dense retrieval + repair Retrieval + repair, with dense retrieval only. | 9/174 | 5.2% | 2% | 3% | 5% | 2 | $0.021 |
| Hybrid retrieval + repair Retrieval plus up to three compiler-feedback repair rounds. | 8/174 | 4.6% | 2% | 3% | 5% | 2 | $0.023 |
| Direct (paraphrased prompt) Direct with a paraphrased prompt (prompt-sensitivity check). | 5/174 | 2.9% | 3% | 3% | 3% | 1 | $0.00403 |
| Hybrid retrieval One draft with eight lemmas retrieved from Mathlib (hybrid retriever) in the prompt. | 3/174 | 1.7% | 2% | 2% | 2% | 1 | $0.012 |
| Direct ×4 Four drafts: the Direct draft plus three resampled with fixed seeds (unseeded repeats were near-identical at this gateway). The equal-budget control for repair: same number of model calls, no feedback. | 2/174 | 1.1% | 1% | 1% | 1% | 1.5 | $0.059 |
| Direct One model draft, checked once. | 1/174 | 0.6% | 1% | 1% | 1% | 1 | $0.030 |
Pre-registered contrasts
Each row compares two configurations on the theorems both attempted. +a/−b counts theorems only the treatment / only the control solved.
| Contrast | n | Difference [95% CI] | +a / −b | p | Holm p |
|---|---|---|---|---|---|
| RQ2 compiler-feedback repair vs one draft Repair vs Direct | 174 | +5.7 pts [+2.3 pts, +9.2 pts] | +10 / −0 | 0.002 | 0.025 |
| RQ2 repair vs independent resampling at equal LLM calls Repair vs Direct ×4 | 174 | +5.2 pts [+2.3 pts, +8.6 pts] | +9 / −0 | 0.004 | 0.047 |
| RQ1 retrieval, single draft Hybrid retrieval vs Direct | 174 | +1.1 pts [−1.1 pts, +3.4 pts] | +3 / −1 | 0.625 | 1.000 |
| RQ1 retrieval, with repair Hybrid retrieval + repair vs Repair | 174 | −1.7 pts [−6.3 pts, +2.9 pts] | +6 / −9 | 0.607 | 1.000 |
| RQ3 planning on top of retrieval + repair Full (plan + retrieval + repair) vs Hybrid retrieval + repair | 174 | +2.9 pts [−0.6 pts, +6.3 pts] | +7 / −2 | 0.180 | 1.000 |
| Primary: full agent vs direct generation Full (plan + retrieval + repair) vs Direct | 174 | +6.9 pts [+3.4 pts, +10.9 pts] | +12 / −0 | <0.001 | 0.007 |
| Ablation: retrieval Full (plan + retrieval + repair) vs Full − retrieval | 174 | +2.3 pts [−1.7 pts, +6.3 pts] | +9 / −5 | 0.424 | 1.000 |
| Ablation: compiler feedback Full (plan + retrieval + repair) vs Full − compiler feedback | 174 | +1.7 pts [+0.0 pts, +4.0 pts] | +3 / −0 | 0.250 | 1.000 |
| Ablation: memory of earlier attempts Full (plan + retrieval + repair) vs Full − memory | 174 | +1.1 pts [+0.0 pts, +2.9 pts] | +2 / −0 | 0.500 | 1.000 |
| Ablation: proof skeleton Full (plan + retrieval + repair) vs Full − skeleton | 174 | +0.0 pts [−3.4 pts, +3.4 pts] | +4 / −4 | 1.000 | 1.000 |
| Retriever: BM25 vs hybrid BM25 retrieval + repair vs Hybrid retrieval + repair | 174 | +2.9 pts [+0.6 pts, +5.7 pts] | +5 / −0 | 0.063 | 0.688 |
| Retriever: dense vs hybrid Dense retrieval + repair vs Hybrid retrieval + repair | 174 | +0.6 pts [−2.3 pts, +3.4 pts] | +4 / −3 | 1.000 | 1.000 |
| LLM vs no-LLM automation Direct vs Template (no LLM) | 174 | −25.9 pts [−32.2 pts, −19.5 pts] | +0 / −45 | <0.001 | <0.001 |
| Prompt sensitivity: paraphrased prompt, direct Direct (paraphrased prompt) vs Direct | 174 | +2.3 pts [+0.6 pts, +4.6 pts] | +4 / −0 | 0.125 | 1.000 |
| Prompt sensitivity: paraphrased prompt, repair Repair (paraphrased prompt) vs Repair | 174 | +0.6 pts [+0.0 pts, +1.7 pts] | +1 / −0 | 1.000 | 1.000 |
By theorem source
| Configuration | Mathlib held-out | Authored |
|---|---|---|
| Template (no LLM) | 10% (12/121) | 64% (34/53) |
| Full (plan + retrieval + repair) | 4% (5/121) | 15% (8/53) |
| Full − skeleton | 4% (5/121) | 15% (8/53) |
| BM25 retrieval + repair | 6% (7/121) | 11% (6/53) |
| Repair (paraphrased prompt) | 7% (8/121) | 8% (4/53) |
| Full − memory | 3% (4/121) | 13% (7/53) |
| Repair | 7% (8/121) | 6% (3/53) |
| Full − compiler feedback | 3% (4/121) | 11% (6/53) |
| Full − retrieval | 6% (7/121) | 4% (2/53) |
| Dense retrieval + repair | 2% (2/121) | 13% (7/53) |
| Hybrid retrieval + repair | 3% (4/121) | 8% (4/53) |
| Direct (paraphrased prompt) | 1% (1/121) | 8% (4/53) |
| Hybrid retrieval | 1% (1/121) | 4% (2/53) |
| Direct ×4 | 0% (0/121) | 4% (2/53) |
| Direct | 0% (0/121) | 2% (1/53) |
By family
| Configuration | Algebra | Category theory | Functions | Inequalities | Number theory | Probability | Sets |
|---|---|---|---|---|---|---|---|
| Template (no LLM) | 33% (10/30) | 21% (5/24) | 54% (7/13) | 23% (7/30) | 17% (5/30) | 17% (4/24) | 35% (8/23) |
| Full (plan + retrieval + repair) | 7% (2/30) | 8% (2/24) | 0% (0/13) | 10% (3/30) | 10% (3/30) | 4% (1/24) | 9% (2/23) |
| Full − skeleton | 0% (0/30) | 8% (2/24) | 8% (1/13) | 10% (3/30) | 10% (3/30) | 4% (1/24) | 13% (3/23) |
| BM25 retrieval + repair | 10% (3/30) | 4% (1/24) | 8% (1/13) | 10% (3/30) | 7% (2/30) | 4% (1/24) | 9% (2/23) |
| Repair (paraphrased prompt) | 13% (4/30) | 8% (2/24) | 0% (0/13) | 13% (4/30) | 7% (2/30) | 0% (0/24) | 0% (0/23) |
| Full − memory | 7% (2/30) | 4% (1/24) | 0% (0/13) | 7% (2/30) | 10% (3/30) | 4% (1/24) | 9% (2/23) |
| Repair | 10% (3/30) | 8% (2/24) | 0% (0/13) | 13% (4/30) | 7% (2/30) | 0% (0/24) | 0% (0/23) |
| Full − compiler feedback | 3% (1/30) | 8% (2/24) | 0% (0/13) | 7% (2/30) | 7% (2/30) | 4% (1/24) | 9% (2/23) |
| Full − retrieval | 10% (3/30) | 4% (1/24) | 8% (1/13) | 10% (3/30) | 3% (1/30) | 0% (0/24) | 0% (0/23) |
| Dense retrieval + repair | 3% (1/30) | 8% (2/24) | 8% (1/13) | 7% (2/30) | 7% (2/30) | 4% (1/24) | 0% (0/23) |
| Hybrid retrieval + repair | 3% (1/30) | 4% (1/24) | 8% (1/13) | 3% (1/30) | 3% (1/30) | 4% (1/24) | 9% (2/23) |
| Direct (paraphrased prompt) | 10% (3/30) | 4% (1/24) | 0% (0/13) | 0% (0/30) | 3% (1/30) | 0% (0/24) | 0% (0/23) |
| Hybrid retrieval | 0% (0/30) | 0% (0/24) | 0% (0/13) | 3% (1/30) | 0% (0/30) | 4% (1/24) | 4% (1/23) |
| Direct ×4 | 0% (0/30) | 4% (1/24) | 0% (0/13) | 0% (0/30) | 3% (1/30) | 0% (0/24) | 0% (0/23) |
| Direct | 0% (0/30) | 4% (1/24) | 0% (0/13) | 0% (0/30) | 0% (0/30) | 0% (0/24) | 0% (0/23) |