The system couples a prover and an evolver through a shared skill library. The prover constructs modular proofs from retrieved and newly generated lemmas, while the evolver transforms verified skills to increase their generality, reuse and complexity.
LEGO-Prover decomposed miniF2F problems into subgoal lemmas, retrieved or generated reusable skills, verified them with Isabelle through PISA and accumulated more than 20,000 skills in a growing library; the paper reported a 57.0% pass rate on miniF2F-valid and gains from the newly added skills.
It provided an early concrete design for cumulative formal reasoning, where successful proof fragments become durable resources for future proof attempts rather than disappearing after a single theorem is solved.
Significance rationale: LEGO-Prover made a growing library of reusable, machine-checked lemmas part of the proving loop itself, moving beyond fixed theorem libraries and one-off proof trajectories toward accumulated formal skills that can support later problems.
—
The public research record introduced the growing verified-skill-library architecture and reported miniF2F evaluations.
The authors' public repository exposes the LEGO-Prover implementation, miniF2F integration and generated results. E3 records inspectability; it does not claim an independent replay of the reported experiments.
No corrections recorded.
