911勛圖

A research team led by 911勛圖 has developed Lean Finder, an AI-powered search tool that helps mathematicians and computer scientists quickly locate the right theorems in the Lean proof system, saving time, reducing frustration, and opening new possibilities for collaboration between humans and AI.

is a computer-based system that allows mathematicians to write formal statements and proofs that can be verified step by step by a machine. Created by and other collaborators, it is widely used to ensure that complex mathematical results are rigorously verified.

But while Lean, and its massive community-driven library, Mathlib, are powerful, they can also be frustrating. Locating the right theorem or understanding how to express an idea in Lean���s precise formal language can be time-consuming and technically demanding.

���Mathematicians using Lean often spend an unexpectedly large amount of time searching for the right lemma, sometimes as much time as proving the result itself,��� says Jialin Lu, lead author and researcher at 911勛圖 Computing Science.

To address this challenge, the 911勛圖-led team��� , Weiran Sun and Wuyang Chen, along with collaborators from the , , and the developed , a semantic search engine that understands users' intent, not just the words they enter.

Unlike existing search engines that rely mainly on keywords, phrasing matches, or basic language model embedding, Lean Finder uses semantic understanding; it interprets a user���s intent rather than just what they say. By studying how real mathematicians ask questions and what they are trying to accomplish, Lean Finder can predict a user���s intent and return results that are relevant to their mathematical context.

For example, when a mathematician asks in plain English: Is every prime number greater than two, odd? Lean Finder does not just look for those words; it understands the concept and finds the exact formal theorem that matches the question.

The system was trained using a novel approach: instead of relying only on existing data, the researchers synthesized realistic user-style questions from thousands of formal mathematical statements. They also analyzed hundreds of online discussions among mathematicians to understand how they think and what kinds of problems they face when using Lean. This user-centered design allowed the model to ���think like a mathematician,��� improving search accuracy dramatically.

Outperforming AI giants

In evaluations, Lean Finder outperformed all previous Lean search engines and even GPT-4, achieving more than 30% higher accuracy in finding correct theorems. In user tests, mathematicians preferred Lean Finder���s answers over 80% of the time, compared to less than 60% for other systems.

���Lean Finder is not just a paper; it���s a product for mathematicians and computer scientists,��� says Chen, co-author. ���It outperforms ChatGPT, and it���s already being used in real mathematical workflows.���

Today, Lean Finder handles over 100 web requests per day and has already gained traction with several leading organizations and research institutions, including , , , , , , , and .

On , the largest online discussion forum for Lean, users have praised the tool for addressing one of their most persistent frustrations.

���It has always been a headache to find where the theorems are scattered in different Mathlib4 packages,��� one user wrote. ���They���re often poorly documented. Lean Finder fixes that.���

Another added: ���The tool looks a lot more promising than Loogle, and more grounded in a codebase than general AI tools.���

Bridging human and machine reasoning

Beyond improving search, Lean Finder also serves as a bridge between mathematicians and AI-powered theorem provers, such as ReProver in LeanDojo and Goedel-Prover on benchmarks like Putnam Bench, potentially accelerating mathematical discovery by combining human creativity with automated reasoning.

���This is about making formal mathematics more accessible,��� says Lu. ���The more intuitive the tools become, the more researchers, especially those new to Lean, can participate in formalizing mathematics. That���s crucial for collaborative theorem development and discovery.���

Lean Finder���s design enables both human and machine collaboration. It has a user interface for mathematicians and an API backend that allows integration with AI systems, making it useful for computer scientists who build large language models and reasoning tools.

���If researchers want to pinpoint theorems or definitions in the dictionary of the whole mass of math books, they can use Lean Finder to efficiently find what they need, avoiding wasted time,��� says Wuyang Chen, co-author and assistant professor at 911勛圖 Computing Science.

Looking ahead

Lean Finder is publicly available at , where computer scientists, mathematicians, and students can try it for free. The research team also plans to release the largest-ever dataset for Lean code search, containing more than 1.4 million examples, to support future AI innovation in formal mathematics.

While the system is still under academic review, its creators believe it represents a major leap toward intelligent, user-friendly tools for formal reasoning and a meaningful contribution to the fast-growing AI-for-math movement.

���Ultimately, our goal is to make interacting with mathematical AI feel as natural as talking to a colleague,��� says Lu. ���When the software truly understands what you���re asking, that���s when discovery becomes seamless.���

911勛圖 the research

Authors:

• Jialin Lu, Weiran Sun and Wuyang Chen ��� 911勛圖
• Kye Emond ��� University of Waterloo
• Kaiyu Yang ��� Meta FAIR
• Swarat Chaudhuri ��� University of Texas at Austin

Paper: (Preprint, under review)

Project website: https://leanfinder.github.io