REVIEW 4 cited by
A Semantic Search Engine for Mathlib4
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
Signed reviews
read the original abstract
The interactive theorem prover Lean enables the verification of formal mathematical proofs and is backed by an expanding community. Central to this ecosystem is its mathematical library, mathlib4, which lays the groundwork for the formalization of an expanding range of mathematical theories. However, searching for theorems in mathlib4 can be challenging. To successfully search in mathlib4, users often need to be familiar with its naming conventions or documentation strings. Therefore, creating a semantic search engine that can be used easily by individuals with varying familiarity with mathlib4 is very important. In this paper, we present a semantic search engine (https://leansearch.net/) for mathlib4 that accepts informal queries and finds the relevant theorems. We also establish a benchmark for assessing the performance of various search engines for mathlib4.
Forward citations
Cited by 4 Pith papers
-
Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph
A graph-of-thought agent with retrieval and a term-grounded semantic checker auto-formalizes research-level math statements in Lean, hitting 68.5% on ProofNet and 6/14 homological conjectures where baselines score 0.
-
Tutte's theorem as an educational formalization project
A Lean formalization of Tutte's theorem is presented and contributed to mathlib, together with a two-phase framework for educational formalization projects.
-
Integrating Rules and Semantics for LLM-Based C-to-Rust Translation
IRENE combines rule-based retrieval, structured summarization, and compiler feedback to improve LLM-based C-to-Rust translation accuracy and safety.
-
Formal Mathematical Reasoning: A New Frontier in AI
Machine-checkable formal proof should become the backbone of AI mathematics, and a five-task, five-level capability roadmap can measure progress toward that goal.
Discussion (0). Continue with ORCID to comment.