An honest assessment of where Bourbaki stands, what the results mean, and what they don't. Updated as we go.
A latent 30-second timeout in the reviewer's final-gate lean_prover call
silently rejected an unknown number of correct proofs on the 2026-05-09 run.
Caught while attempting to reproduce a known-good result.
The reviewer node calls lean_prover once on the assembled standalone source
to verify a proposal before reporting it as solved. Until commit
7b07c07, that call
passed no timeout kwarg and inherited the function's 30s default. Standalone
lake env lean with import Mathlib needs 60-180s on a cold cache —
the REPL stays warm between proofs, but each standalone compile starts fresh.
On a quiet machine the 30s often happened to be enough. On a loaded one, the timeout fired silently — the reviewer's final gate returned failure, the loop reported the problem as FAILED, and the actual code-level state was "the proposer generated a correct proof but we couldn't compile it fast enough."
Trying to re-run mathd_algebra_10 (a single-step by norm_num problem that
solved on iteration #1 in both the Apr 25 and May 9 runs) under heavy CPU load
(uptime showed load average ~17). Result: 0/1 verified, attempts=4.
Same code that scored 9/10 and 22/35 now scored 0/1.
Commit 7b07c07
bumps the reviewer's lean_prover call to timeout=240, matching what the
outer benchmark verifier (_verify_with_lean_prover) already used.
- 9/10 (Apr 25, 10-problem subset): ran on a quiet machine. Almost
certainly not affected — the headline number was reproducible at the time
and the 1 miss (
mathd_algebra_31) is a genuinely hard problem. - 22/35 (May 9, 35-problem stratified): this is a lower bound. Some of the 13 failures may have been correct proofs that timed out at the 30s gate. The actual capability of the loop on that subset is somewhere between 62.9% and 100%. We won't know until the re-run lands.
- All earlier numbers (6.2%, 25.8%, 28.6%, 40%, etc.) used the heuristic search pipeline, not the proposer-builder-reviewer loop, and are unaffected by this bug.
- Default timeouts on functions called by other functions are landmines.
The
lean_prover30s default makes sense for interactive tool use from the agent. It does not make sense for a programmatic final-gate call from the reviewer. The two call sites have different latency requirements. Add explicittimeout=kwargs at every site rather than relying on the default to be "right for everyone." - System load can mask latent bugs. The same code that scored 22/35 on a quiet workstation scored 0/1 under load. Always run benchmarks on a dedicated/quiet machine; otherwise you're measuring kernel scheduler pressure as much as model capability.
- Reproducibility is a feature. Trying to reproduce a known-good result
surfaced this bug. If the May 14 reproduction had been skipped on the
assumption that "the May 9 number is fine," the bug would have remained
latent and
v0.3.0would have shipped with it.
Re-run on the same 35-problem subset is tracked in issue #19; it blocks the full 244-problem run (#14) and the v0.3.0 release (#15).
RETRACTED 2026-05-14. The 91.8% / 94.3% numbers below were inflated ~15× by REPL false positives. The v0.2.0 and v0.2.1 GitHub releases now carry "RETRACTED (inflated numbers)" titles. The 2026-02-22 audit further down cuts the verified rate to 6.2% on the same code; the current proposer-builder-reviewer loop is at 9/10 and 22/35 on smaller samples (see ARCHITECTURE.md "Benchmark" section). Text below is preserved verbatim for historical context — every benchmark number in this section is invalid.
-
94.3% on miniF2F test split using an off-the-shelf general-purpose LLM (GLM-5) with no fine-tuning, no custom training data, no reinforcement learning.
-
The baseline (92.6% without the LLM) is pure tactic search — no neural model at all, just a heuristic search tree over Lean tactics. That baseline alone beats Aristotle (90%) and ties with Goedel-Prover V2 (90.4%), systems that use dedicated 200B+ transformers or fine-tuned 32B models.
-
The architecture is a coding agent with tools, not a specialized theorem proving model. Best-first search + Lean REPL + off-the-shelf LLM coordination. That's a fundamentally different (and more general) approach than training a dedicated prover.
-
Open source, reproducible. No proprietary training data, no private model weights. Anyone with Lean 4 + Mathlib + an LLM API key can reproduce the results.
-
HILBERT is at 99.2%. The remaining 5pp gap is real and hard. It likely requires a trained value/policy model (Goedel-V2-32B) and significantly more compute per problem.
-
Our search tree benefits from Lean/Mathlib being very good. Many of the 226 baseline solves are Lean's automation (norm_num, omega, simp, ring, linarith) doing the heavy lifting, not Bourbaki. The search tree's contribution is systematic exploration of tactic combinations, not mathematical insight.
-
The multi-agent coordinator only adds 4-6 problems per split. The LLM contribution is relatively small compared to the search tree. Most of the result comes from tactic automation, not from language model reasoning.
-
miniF2F is a well-studied benchmark. Being near the top on miniF2F doesn't mean we can handle IMO competition problems the way Aristotle or AlphaProof can. Those systems solve open problems; we solve formalized textbook/competition problems where the answer is known.
-
We haven't published a paper or had peer review. The reference systems (HILBERT, Aristotle, DeepSeek-Prover) have published at NeurIPS, ICML, etc. Our results are self-reported benchmark runs.
-
The test split (94.3%) is stronger than the valid split (91.8%). This is unusual — typically you'd expect similar or slightly worse performance on the test split. It could indicate variance or that the test split problems happen to align better with our tactic generators.
"94.3% on miniF2F test split, competitive with Aristotle and Goedel-V2, using search + off-the-shelf LLM, no fine-tuning."
That's the claim. Nothing more, nothing less.
A small open-source project with a coding-agent architecture and no custom training can be competitive with well-funded labs on the standard formal theorem proving benchmark. Good search + good tools + off-the-shelf LLM coordination gets you surprisingly far.
| Gap | Impact | What would close it |
|---|---|---|
| Trained value model | +3-5pp | Fine-tune 8B+ model on proof search traces (needs GPU) |
| Pass@N sampling | +1-2pp | Run 32-256 attempts per problem, take first success (needs compute) |
| Deeper decomposition | +1-2pp | More LLM sketch iterations, better subgoal splitting |
| Competition-level reasoning | qualitative | Test-time training (Aristotle), RL (DeepSeek) |
| System | miniF2F Valid | miniF2F Test | Model | Training | Open Source |
|---|---|---|---|---|---|
| HILBERT | 99.2% | — | Goedel-V2-32B | Fine-tuned | Yes (Apache 2.0) |
| Bourbaki | 91.8% | 94.3% | GLM-5 (off-the-shelf) | None | Yes (MIT) |
| Goedel-Prover V2 | 90.4% | — | Custom 8B/32B | Self-correction RL | Partial |
| Aristotle | 90% | — | Custom 200B | MCGS + test-time training | No |
| DeepSeek-Prover V2 | 88.9% | — | DeepSeek-V2 | GRPO RL | No |
35-problem stratified sample across all miniF2F valid categories, with all
correctness fixes applied: _build_proof_code (#2), tactic blocklist (#3),
inline lean_prover verification (#6), benchmark guardrails (#9), and
expand() early-return fix.
| Category | Verified | Rate |
|---|---|---|
| mathd | 8/15 | 53% |
| algebra | 1/5 | 20% |
| unknown (AMC) | 1/5 | 20% |
| aime | 0/3 | 0% |
| imo | 0/3 | 0% |
| induction | 0/2 | 0% |
| numbertheory | 0/2 | 0% |
-
Multi-step proofs now verify.
mathd_algebra_192(4 tactics:aesop → field_simp → ring → norm_num) andmathd_algebra_234(2 tactics:simp [pow_succ] → nlinarith) both verified. Previously all 63 verified solves were single-tactic. -
Inline verification catches false positives during search. The
induction n with | zero => simp | succ n ih => simp_allpattern triggered 18 false positives on a single problem. All caught and rejected before reaching results. -
Zero false positives in final results. REPL-reported == verified for the first time.
-
induction...simp_allis a false positive factory. Every problem with an induction-shaped goal gets poisoned. Each verification costs ~6s. Needs blocklisting (#10). -
The overall rate (28.6%) is not meaningfully different from 25.8%. The fixes improved correctness and caught a new solve (
mathd_algebra_547), but the verified rate didn't jump. The 63/244 baseline was already accurate.
| System | miniF2F Valid | Verified? |
|---|---|---|
| HILBERT | 99.2% | Yes (published) |
| BFS-Prover-V2 | 95.08% | Yes (published) |
| Goedel-V2 | 90.4% | Yes (published) |
| Aristotle | 90% | Yes (published) |
| DeepSeek-V2 | 88.9% | Yes (published) |
| Bourbaki | ~26-29% | Yes (lean_prover verified) |
Full miniF2F valid split with lean_prover verification (whole-file compilation, 150s timeout per problem). Result: 15/244 (6.2%).
| Category | Verified | Rate |
|---|---|---|
| algebra | 6/18 | 33% |
| unknown (AMC/misc) | 3/48 | 6% |
| mathd | 6/130 | 5% |
| aime | 0/12 | 0% |
| imo | 0/20 | 0% |
| induction | 0/8 | 0% |
| numbertheory | 0/8 | 0% |
Only standard Lean automation tactics produce valid proofs:
| Tactic | Verified Solves |
|---|---|
ring |
5 |
rfl |
3 |
simp |
3 |
norm_num |
1 |
linarith |
1 |
nlinarith |
1 |
field_simp |
1 |
The search tree's most common "proof" tactic — exact ⟨_, _⟩ — is entirely
bogus. It was used on 100+ problems and NONE verify. The REPL reports "no
remaining goals" but lean_prover rejects with "Insufficient number of fields
for ⟨...⟩ constructor."
The anonymous constructor ⟨_, _⟩ asks Lean to infer the arguments. In the
REPL's sorry-initialized proof state, Lean's elaborator sometimes closes the
goal display without constructing a valid proof term. In standalone compilation,
this correctly fails.
The previous claims (91.8% valid, 94.3% test) were entirely from REPL false positives. The actual verified rate is 6.2% — only standard automation tactics that don't depend on the proof state context.
The search tree architecture is sound but the proof detection is broken. The fix is to either:
- Stop using
exact ⟨_, _⟩as a candidate tactic - Add lean_prover verification inline during search (expensive but correct)
- Fix the REPL detection to match standalone compilation behavior
| System | miniF2F Valid | Verified? |
|---|---|---|
| HILBERT | 99.2% | Yes (published, peer-reviewed) |
| BFS-Prover-V2 | 95.08% | Yes (published) |
| Goedel-V2 | 90.4% | Yes (published) |
| Aristotle | 90% | Yes (published) |
| DeepSeek-V2 | 88.9% | Yes (published) |
| Bourbaki | 6.2% | Yes (lean_prover verified) |
We ran PutnamBench (672 Putnam competition problems). The initial run reported 95.4% (641/672). Audit revealed this was entirely inflated:
- 224 answer-sorry problems had
abbrev ... := sorryplaceholders. With an unconstrained answer, theorems are trivially satisfiable. Not valid solves. - 49 suspicious tactics like
exact Lean.defaultMaxRecDepth— Lean internals, not mathematical proofs. - All 317 remaining "proofs" failed lean_prover verification.
Our search tree uses the Lean REPL to detect proof completion. The REPL reported
"no remaining goals" for tactics like simp, exact mem_of, norm_num on
PutnamBench problems. But when the same code was compiled as a standalone Lean
file via lean_prover, every single proof was rejected.
This is a systematic false positive specific to PutnamBench's more complex formulations. The REPL's sorry-initialized proof states have different elaboration context than standalone compilation. Tactics that appear to close goals in the REPL don't actually produce valid proof terms.
| Benchmark | REPL-reported | lean_prover verified | Status |
|---|---|---|---|
| miniF2F valid (v0.2.1 code) | 224/244 (91.8%) | 15/244 (6.2%) | Re-verified Feb 22 — claim was inflated ~15× |
| miniF2F valid (v0.2.2 code) | — | 63/244 (25.8%) | Mar 8 baseline · same code with REPL pipe-recovery + tactic blocklist |
| miniF2F valid (35-problem stratified, post-loop) | — | 22/35 (62.9%) | May 9 · proposer-builder-reviewer loop · 0 false positives |
| miniF2F valid (full 244, post-loop) | — | Pending | tracked in #14 |
| miniF2F test (v0.2.1 code) | 230/244 (94.3%) | Not re-verified | claim retracted; full test re-run pending #14 |
| PutnamBench (theorem-only, pre-Phase-3) | 317/326 | 0/326 (0%) | All false positives |
| PutnamBench (answer-sorry) | 224/346 | Excluded | Need answer generation |
| PutnamBench (5-problem dry run, new loop) | — | 0/5 | Was blocked on #13 (pydantic_ai/z.ai adapter bug); #13 now closed by commit 66cba4c (args_as_dict shim). Re-run pending. |
miniF2F problems are simpler — standard competition math with straightforward
type signatures. The REPL detection works correctly for these. Spot-checked
norm_num proofs verified successfully with lean_prover.
PutnamBench problems use deeper Mathlib types (MeasureTheory, Topology, EuclideanSpace), complex dependent types, and longer theorem statements. The gap between REPL elaboration and standalone compilation is wider for these.
- Always verify with lean_prover. REPL-based detection is an approximation.
- Set verification timeout to 150s+. Mathlib import alone takes 75-100s.
- Answer-sorry problems need answer generation. Can't just skip them.
- Filter non-proof tactics. Lean internals aren't mathematical proofs.
- PutnamBench is genuinely harder. HILBERT's 70% with a trained 32B model puts our 0% in context — these problems are beyond tactic automation.
The Feb 18 v0.2.1 miniF2F numbers (91.8% valid / 94.3% test) were inflated
~15×. The Feb 22 audit replaced them with 6.2% verified. The v0.2.2 release
(Mar 8) lifted the honest number to 25.8% on the full 244 split. The current
architecture (proposer-builder-reviewer loop, commits 49211ce...2113629)
is at 22/35 (62.9%) on a stratified sample as of May 9 — the full 244 re-run
is the v0.3.0 release blocker, tracked in
issue #14.
The v0.2.0 and v0.2.1 GitHub release titles were updated to
"v0.2.x — RETRACTED (inflated numbers)" on 2026-05-14. The git tags
themselves and the in-repo CHANGELOG.md entries also carry inline
RETRACTED block-quotes. Tagging a clean v0.3.0 release on top of the
new loop is tracked in
issue #15 (open;
blocked on the full 244-problem run, issue #14).
This document exists to keep us honest. Update it whenever results change.