LeanDojo is an open-source platform for proving mathematical theorems using language models.
Automated theorem proving (ATP) is a task that generates proofs for theorems formulated in formal logic. It is useful for formal mathematics and supports formal verification, which ensures the correctness and security of high-risk applications.
However, ATP is challenging due to its large search space. Therefore, Interactive Theorem Proving (ITP) has emerged as an alternative. In ITP, proofs are generated by mathematicians interacting with software tools called proof assistants.
Machine learning could automate this process, opening up a new way of proving theorems.
Large Language Models could automate theorem proving
Large language models combined with proof assistants such as Lean are a candidate for this process.
However, existing methods are difficult to reproduce or evolve due to proprietary code, data, and high computational requirements, according to a team of researchers from Caltech, Nvidia, MIT, UC Santa Barbara, and UT Austin.
To address this, they created LeanDojo, an open-source platform for proving mathematical theorems using language models.
LeanDojo and ReProver open the door for further research
LeanDojo provides two key features for learning-based theorem proving: data extraction and programmatic interaction of models with Lean, a widely used proof assistant. According to the researchers, LeanDojo is the first tool that can reliably interact with Lean, which should significantly reduce proof errors.
LeanDojo also addresses a key bottleneck in theorem proving: premise selection. The team demonstrates this with ReProver (Retrieval-Augmented Prover), a language model-based prover that generates a proof strategy based on a few premises retrieved from Lean's math library.
According to the team, ReProver outperforms some other methods, proving a significant percentage of theorems in the LeanDojo benchmark, as well as in two existing datasets, MiniF2F and ProofNet. ReProver can also prove theorems for which there is currently no proof in Lean, making it a useful tool for extending existing math libraries in Lean.
Language models to co-author math by 2026?
The team is also releasing a benchmark built with LeanDojo that includes nearly 97,000 theorems from Mathlib, as well as a plugin for ChatGPT.
Mathematician Terence Tao recently predicted that language models using external tools could become trusted co-authors in math and other sciences by 2026. LeanDojo and ReProver show what such tools could look like, and now offer other researchers a basis for improvement.
More information is available on the LeanDojo site.
