LeanAide: AI for Lean & Mathematics

Sat, Feb 8, 2025

LeanAide or LeanAIde (accidental pun) is work (in progress) to build AI based tools to work with the Lean Theorem Prover. Our goal is to build tools for:

• Users of the Lean Prover by using AI tools.
• Mathematicians to use both Lean and AI. The role of Lean for mathematicians whose goal is not formalizing, but discovery is:
  • To filter out incorrect statements from models, and even give feedback on errors and missing details.
  • To organize mathematics as it develops. Mathematical discovery is not simply answering a question but involves decomposition of problems, experimentation etc. Lean facilitates accumulating mathematical knowledge in a modular fashion.

The core technique we use is Autoformalization which is translating informal mathematical statements to formal statements in a proof assistant (Lean Prover in our case). This is used both directly to provide tools and indirectly to generate proofs by translation from natural language proofs generated by Large Language models.

I spoke about LeanAide in a Lecture at Lean Together 2025:

In the 3-4 weeks after the lecture, we have managed to finish two significant steps:

• Change of design to a Server-Client model.
  • This means that LeanAide is actually not hard to use in a Lean project.
  • Further, this opens the way to use the server with a different client, including where Lean is kept completely in the background for uses in mathematical education and research.
• A skeleton of larger-scale autoformalization code, done in what seems a correct and extendable way.
  • We need to build on this by testing, finding limitations and errors, fixing and expanding etc.
  • The code works at a single theorem and proof level. We need to scale up further.
  • However, scaling from the basic code one hopes is just a matter of work and will not face fundamental difficulties.

The rest of this blog is an introduction to LeanAide. It was drafted (almost single-shot) from my lecture linked above by Gemini Flash 2.0-experimental-thinking with apps. I had to fix some errors, but most of the writing was done for me.

LeanAide: Bridging the Gap Between Natural Language and Formal Mathematics with AI

LeanAide is a system I’ve developed (with collaborators) to explore how AI can make formalizing mathematics in Lean more accessible and efficient. My goal isn’t just full automation of formalization, but to create a practical and interactive environment where AI can assist mathematicians at every stage. This assistance ranges from helping beginners learn Lean syntax to supporting experts in tackling complex mathematical formalization.

What is LeanAide?

LeanAide is an AI-powered system that aims to make formalizing mathematics in Lean more approachable and more productive. It’s built around the idea of pragmatic autoformalization. This means we focus on the practical usefulness of AI in translating natural language mathematics into Lean code. Rather than solely aiming for perfect automated translation accuracy, we prioritize creating tools that are genuinely helpful and interactive for users throughout the formalization process.

How Does LeanAide Work?

LeanAide uses AI, specifically GPT 4o, to connect the way mathematicians naturally express themselves with the rigorous formal language of Lean. The user can use a different model in place of GPT-4o. Here are the core functionalities of our system:

• Deep Integration with Lean: LeanAide is deeply integrated with Lean using Meta-programming. This is both used to improve the quality of translation and usability of the tools.

• Natural Language to Lean Code Translation: LeanAide includes tools that translate theorem statements and definitions written in natural language into Lean code, and convenient syntax #theorem and #def to use the tools. This is designed to be helpful for those new to Lean syntax and for more experienced users who want a quick way to translate mathematical ideas into code.

• Automated Documentation: Our system can automatically generate docstrings for Lean code. This improves the readability and makes the code easier to maintain.

• Mathlib Integration: LeanAide is integrated with Lean’s mathlib (mathematical library). It uses mathlib to find relevant documentation strings and examples. This context helps improve the quality of translations by giving the AI model relevant examples to draw from.

• Prompting and Post-processing with GPT 4o: We use GPT 4o for translations, with a focus on creating effective prompts and using post-processing techniques to refine the output. Instead of fine-tuning models, we emphasize carefully designed prompts and filters to ensure that only valid Lean code is produced. Invalid code responses are discarded.

• Iterative Refinement: LeanAide uses elaboration filters, manages language model “chattiness,” and includes autocorrections to improve the accuracy and reliability of the AI-generated code. It also groups responses and uses Lean’s aesop tactic to check for equivalent outputs and select the most suitable translation.

• Informalization for Training Data Generation: LeanAide can translate formal theorems back into natural language (“informalization”). This process is useful for creating more training data, which in turn helps improve the system’s translation capabilities.

• Handling Ambiguity and Missing Definitions: LeanAide incorporates methods to address missing definitions, logical inconsistencies, and ambiguous syntax. This makes it more capable of handling the nuances of real-world mathematical language.

• Iterative Formalization for Complex Tasks: For larger, more complex formalization projects, LeanAide uses an iterative approach. Proofs are broken down into smaller, more manageable parts. Language models assist in proving each part, and these proofs are then translated into a structured JSON format before being autoformalized into Lean code. Rule-based tactics are then used to complete the proofs.

How LeanAide Helps with Lean and Mathematics:

LeanAide offers several advantages for Lean users and the broader field of mathematics:

• Easier Entry to Lean: By offering tools for translating natural language to Lean code and providing interactive assistance, LeanAide aims to make Lean more accessible for newcomers. It can help new users learn Lean syntax and understand mathematical terminology within the context of formalization.
• Faster Formalization Process: For those already familiar with Lean, LeanAide can speed up the formalization process. It can provide initial translations, automate documentation, and assist with breaking down complex proofs. This allows mathematicians to concentrate on the higher-level aspects of reasoning and problem-solving.
• Draft formalizations LeanAide can generate initial draft translations that can then be reviewed and refined, similar to successful methods used in past porting efforts from Lean 3 to Lean 4.
• Connecting Informal and Formal Mathematics: LeanAide aims to create a better connection between how mathematicians naturally think and write mathematics and the formal reasoning required by interactive theorem provers. This can make the formalization process feel more natural and intuitive.
• Potential for Mathematical Exploration: I believe that Lean, enhanced by AI tools like LeanAide, can become not just a tool for formalization but also for mathematical exploration. By making formalization more efficient and accessible, LeanAide can empower mathematicians to explore and develop new mathematical ideas within a rigorous and verifiable framework.

Future Directions:

The development of LeanAide is ongoing. Our future work will focus on:

• Improving the quality of code generation and translation at both the sentence and proof levels.
• Improving the user experience and making the system easier to install and use.
• Exploring how to scale up autoformalization to handle entire mathematical documents.

As mentioned at the beginning of this post, the second of this is I believe done and there has been some progress on the third, including a key step.

LeanAide is a step towards integrating AI more deeply into mathematical workflows. By concentrating on practical tools and interactive assistance, we hope to make Lean more accessible and efficient, and ultimately, a more powerful tool for mathematical work. As both Lean and AI continue to evolve, systems like LeanAide may help to create a future where mathematicians can more easily combine informal and formal methods to advance mathematical understanding.