51社区黑料

A research team led by 51社区黑料 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鈥檚 precise formal language can be time-consuming and technically demanding.

鈥淢athematicians 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 51社区黑料Computing Science.

To address this challenge, the SFU-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鈥檚 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鈥檚 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 鈥渢hink 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鈥檚 answers over 80% of the time, compared to less than 60% for other systems.

鈥淟ean Finder is not just a paper; it鈥檚 a product for mathematicians and computer scientists,鈥� says Chen, co-author. 鈥淚t outperforms ChatGPT, and it鈥檚 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.

鈥淚t has always been a headache to find where the theorems are scattered in different Mathlib4 packages,鈥� one user wrote. 鈥淭hey鈥檙e often poorly documented. Lean Finder fixes that.鈥�

Another added: 鈥淭he 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.

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

Lean Finder鈥檚 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.

鈥淚f 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 51社区黑料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.

鈥淯ltimately, our goal is to make interacting with mathematical AI feel as natural as talking to a colleague,鈥� says Lu. 鈥淲hen the software truly understands what you鈥檙e asking, that鈥檚 when discovery becomes seamless.鈥�

51社区黑料 the research

Authors:

• Jialin Lu, Weiran Sun and Wuyang Chen 鈥� 51社区黑料
• 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