LEGO-Prover
Grows a persistent library of verified Isabelle/HOL helper lemmas while proving theorems block-by-block.
The loop
- Proposes
A prover LLM decomposes a theorem into candidate helper lemmas and formal Isabelle proof sketches, while an evolvar LLM mutates verified lemmas in the skill library.
- Judged by
The Isabelle/HOL kernel and Sledgehammer verify every proposed lemma and proof sketch.
- Steers
Verified lemmas are indexed into a growing modular skill library and retrieved via semantic search to simplify subsequent theorems.
Headline result
Raised miniF2F-valid pass@100 to 57.0% and miniF2F-test to 50.0% in Isabelle/HOL, accumulating thousands of reusable verified lemmas.
What this does not prove
Library quality depends on pruning redundant or overly specialized lemmas so retrieval stays sharp.
How it generalizes the harness
- The algorithm is the solver
- A domain authority judges
- The output outlives the model
- Search over a population
- An infallible formal kernel
The Isabelle/HOL kernel gates admission into a persistent, evolving library of formally verified mathematical lemmas.
Classification
| What it proposes | Proof |
|---|---|
| Generative model | GPT-3.5 / LLaMA-2 prover and lemma-evolver agents |
| Algorithmic authority | Isabelle/HOL proof kernel and Sledgehammer ATP |
| Feedback | Proof state |
| What gets updated | Population of candidates and prompt context |
| When it runs | At inference time |
| Validity | Formal (machine-checked) |
| Evidence | Code released |
| Lineage | Successor |