Primary evidence
- Baldur: Whole-Proof Generation and Repair with Large Language ModelsS1 · Primary research · Paper · 2023-03-08
- Baldur: Whole-Proof Generation and Repair with Large Language ModelsS1 · Primary research · Other source · 2023-12-06
Baldur generates and repairs whole formal proofs with language models
Instead of predicting one proof step and searching over continuations, Baldur fine-tuned language models to generate an entire proof in one pass. A separate repair model then received a failed proof attempt together with proof-assistant error feedback and proposed a corrected proof.
What happened?
On a benchmark of 6,336 Isabelle/HOL theorems, Baldur generated whole proofs and repaired failed generations, proving an additional 8.7% of theorems beyond Thor; the paper reported that Baldur and Thor together proved 65.7% fully automatically.
Why it matters
The work made complete-proof synthesis and feedback-driven repair a credible formal-reasoning pattern, complementing search-heavy theorem provers and anticipating later generate-check-revise workflows.
Significance rationale: Baldur established whole-proof generation plus checker-guided proof repair as a distinct alternative to step-by-step formal proof search, showing that a transformer could emit complete Isabelle/HOL proofs and use failed attempts and error messages as repair context.
Historical context
Earlier developments
Later developments
—
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E2 · Research record
- AI role
- AI primary, human verified
- Formal assurance
- No formal assurance
Contribution & verification
- Mathematical novelty
- Tooling only
- Interface
- Formal, Symbolic, Hybrid
- AI contribution
- Fine-tuned language models generated complete candidate proofs and repaired failed attempts using checker feedback; Isabelle/HOL mechanically accepted or rejected the resulting proof text.
- Human contribution
- Researchers designed the whole-proof and repair training setup, assembled the evaluation protocol, trained the models and analyzed performance against prior theorem-proving systems.
- Verification
- Paper released · E2 · Research record · No formal assurance
- Last reviewed
- 2026-09-11
Technical details
- Systems
- baldur, isabelle-hol
- Organizations
- —
- Problems
- automated-theorem-proving
- Methods
- whole-proof-generation, proof-repair, language-models, proof-assistant-feedback
Sources & artifacts
- Baldur: Whole-Proof Generation and Repair with Large Language ModelsS1 · Primary research · Paper · accessed 2026-09-11
- Baldur: Whole-Proof Generation and Repair with Large Language ModelsS1 · Primary research · Other source · accessed 2026-09-11
Verification history
- 2023-03-08 · Paper released · E2 · Research record
The public research record reports the whole-proof generation, repair method and Isabelle/HOL evaluation. This status records the paper and does not imply independent Chronicle verification or a public replay artifact.
Corrections
No corrections recorded.