Lean Finder: Semantic Search for Mathlib That Understands User Intents

• URL: http://arxiv.org/abs/2510.15940v1
• Date: Wed, 08 Oct 2025 19:51:49 GMT
• Title: Lean Finder: Semantic Search for Mathlib That Understands User Intents
• Abstract summary: Lean Finder is a semantic search engine for Lean and mathlib.<n>It understands and aligns with the intents of mathematicians.<n>It is compatible with LLM-based theorem provers, bridging retrieval with formal reasoning.
• Score: 19.454158593716578
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We present Lean Finder, a semantic search engine for Lean and mathlib that understands and aligns with the intents of mathematicians. Progress in formal theorem proving is often hindered by the difficulty of locating relevant theorems and the steep learning curve of the Lean 4 language, making advancement slow and labor-intensive. Existing Lean search engines, though helpful, rely primarily on informalizations (natural language translation of the formal statements), while largely overlooking the mismatch with real-world user queries. In contrast, we propose a user-centered semantic search tailored to the needs of mathematicians. Our approach begins by analyzing and clustering the semantics of public Lean discussions, then fine-tuning text embeddings on synthesized queries that emulate user intents. We further align Lean Finder with mathematicians' preferences using diverse feedback signals, encoding it with a rich awareness of their goals from multiple perspectives. Evaluations on real-world queries, informalized statements, and proof states demonstrate that our Lean Finder achieves over $30\%$ relative improvement compared to previous search engines and GPT-4o. In addition, Lean Finder is compatible with LLM-based theorem provers, bridging retrieval with formal reasoning. Lean Finder is available at: https://leanfinder.github.io

Related papers

• Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics [20.90238876313568]
  Large Language Models (LLMs) produce subtle errors that evade human detection.<n>Recent trends indicate that general-purpose LLMs now outperform smaller models explicitly fine-tuned for Lean.<n>We introduce an agentic autoformalization framework powered by general coding LLMs.
  arXiv  Detail & Related papers  (2026-06-30T05:05:03Z)
• LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
  Large Language Models (LLMs) exhibit strong informal mathematical reasoning but struggle to generate verifiable proofs in formal languages like Lean.<n>We present LEAP, an agentic framework that enables general-purpose foundation models to achieve state-of-the-art performance on automated formal theorem proving.
  arXiv  Detail & Related papers  (2026-06-02T08:16:42Z)
• MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics [51.65118519899584]
  We introduce MathlibLemma, the first LLM-based multi-agent system to automate the discovery and formalization of mathematical folklore lemmas.<n>We further construct the MathlibLemma benchmark, a suite of 4,028 type-checked Lean statements spanning a broad range of mathematical domains.
  arXiv  Detail & Related papers  (2026-01-30T15:24:42Z)
• LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories) [7.871706113805829]
  LeanCat is a Lean benchmark for category-theoretic formalization.<n>Part I: 1-Categories contains 100 fully formalized statement-level tasks.<n>Part II: LeanBridge uses LeanExplore to search Mathlib and observe consistent gains over single-model baselines.
  arXiv  Detail & Related papers  (2025-12-31T11:33:29Z)
• DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems [14.568293842955065]
  DRIFT is a framework that decomposes informal mathematical statements into smaller, more tractable ''sub-components''<n>It retrieves illustrative theorems to help models use premises more effectively in formalization tasks.<n>We evaluate DRIFT across diverse benchmarks (ProofNet, ConNF, and MiniF2F-test) and find that it consistently improves premise retrieval.
  arXiv  Detail & Related papers  (2025-10-12T21:42:04Z)
• LeanExplore: A search engine for Lean 4 declarations [0.0]
  This paper introduces LeanExplore, a search engine for Lean 4 declarations.<n>LeanExplore enables users to semantically search for statements across select Lean 4 packages.
  arXiv  Detail & Related papers  (2025-06-04T16:09:54Z)
• The quasi-semantic competence of LLMs: a case study on the part-whole relation [53.37191762146552]
  We investigate knowledge of the emphpart-whole relation, a.k.a. emphmeronymy.<n>We show that emphquasi-semantic'' models have just a emphquasi-semantic'' competence and still fall short of capturing deep inferential properties.
  arXiv  Detail & Related papers  (2025-04-03T08:41:26Z)
• FLARE: Faithful Logic-Aided Reasoning and Exploration [47.46564769245296]
  We introduce a novel approach for traversing the problem space using task decompositions.<n>We use the Large Language Models to plan a solution, soft-formalise the query into facts and predicates using a logic programming code.<n>Our method allows us to compute the faithfulness of the reasoning process w.r.t. the generated code and analyse the steps of the multi-hop search without relying on external solvers.
  arXiv  Detail & Related papers  (2024-10-14T19:39:11Z)
• A Semantic Search Engine for Mathlib4 [3.4826238218770813]
  We present a semantic search engine for mathlib4 that accepts informal queries and finds the relevant theorems.<n>We also establish a benchmark for assessing the performance of various search engines for mathlib4.
  arXiv  Detail & Related papers  (2024-03-20T05:23:09Z)
• AlignedCoT: Prompting Large Language Models via Native-Speaking Demonstrations [52.43593893122206]
  Alignedcot is an in-context learning technique for invoking Large Language Models. It achieves consistent and correct step-wise prompts in zero-shot scenarios. We conduct experiments on mathematical reasoning and commonsense reasoning.
  arXiv  Detail & Related papers  (2023-11-22T17:24:21Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  Large language models (LLMs) have shown promise in proving formal theorems using proof assistants such as Lean. Existing methods are difficult to reproduce or build on, due to private code, data, and compute requirements. This paper introduces LeanDojo: an open-source Lean toolkit consisting of toolkits, data, models. We develop ReProver: an LLM-based prover augmented with retrieval for selecting premises from a vast math library.
  arXiv  Detail & Related papers  (2023-06-27T17:05:32Z)
• Evaluating Language Models for Mathematics through Interactions [116.67206980096513]
  We introduce CheckMate, a prototype platform for humans to interact with and evaluate large language models (LLMs) We conduct a study with CheckMate to evaluate three language models (InstructGPT, ChatGPT, and GPT-4) as assistants in proving undergraduate-level mathematics. We derive a taxonomy of human behaviours and uncover that despite a generally positive correlation, there are notable instances of divergence between correctness and perceived helpfulness.
  arXiv  Detail & Related papers  (2023-06-02T17:12:25Z)
• Query Rewriting for Retrieval-Augmented Large Language Models [139.242907155883]
  Large Language Models (LLMs) play powerful, black-box readers in the retrieve-then-read pipeline. This work introduces a new framework, Rewrite-Retrieve-Read instead of the previous retrieve-then-read for the retrieval-augmented LLMs.
  arXiv  Detail & Related papers  (2023-05-23T17:27:50Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.