Baldur

By University of Massachusetts Amherst, Google, 2023. Proofs. Verifier-guided repair.

Generates whole-function Isabelle/HOL proofs and uses the prover error message to repair broken proofs.

The loop

Proposes
A language model generates a complete Isabelle/HOL proof script for a target theorem.
Judged by
The Isabelle proof assistant executes the script and returns an error message when the proof fails.
Steers
A repair model conditions on the statement, the whole failed proof and the Isabelle error message to synthesize a corrected proof.

Proved 47.9% of theorems in the Isabelle Archive of Formal Proofs benchmark (65.7% when combined with Thor Sledgehammer).

Single-round error repair struggles on deep multi-lemma obligations where the initial proof sketch chooses the wrong induction variable.

The Isabelle/HOL kernel acts as the formal oracle whose error messages drive whole-proof synthesis and repair.

Classification of Baldur
What it proposes	Proof
Generative model	Minerva-based proof generation and repair LLMs
Algorithmic authority	Isabelle/HOL proof assistant and Sledgehammer ATP
Feedback	Verifier errors
What gets updated	Prompt context
When it runs	At inference time
Validity	Formal (machine-checked)
Evidence	Experiments reported
Lineage	Original system