Lean State Search
Search Mathlib Theorem with Proof States
News
2025/03/07 Update: LeanSearchClient now supports query Lean State Search from within Lean.
2025/03/05 Update: Lean State Search is now publicly available!
About
Lean State Search is an innovative search engine powered by a pretrained model, specifically designed to help mathematicians and Lean4 users efficiently search Mathlib theorems using proof states. It is developed by the AI4Math team at Renmin University of China.
We collect user feedbacks to improve our model. These feedbacks will also be publicly available and continuously updated.
Usage
Our search engine will parse the proof states from the Lean infoview into arguments and goals. The special token ⊢ is required. Here is a valid query example:
n : ℕ ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m h : 2 ≤ n np : ¬Nat.Prime n ⊢ ∃ p, Nat.Prime p ∧ p ∣ n
You can copy the proof states directly from the infoview. It is also recommended to only keep the relevant hypotheses for better accuracy.
Resources
Model & Code:
Research Paper:
Coming Soon: Self-hosting and custom deployment options for the search engine!
Citation
@misc{tao2025assistingmathematicalformalizationlearningbased,
title={Assisting Mathematical Formalization with A Learning-based Premise Retriever},
author={Yicheng Tao and Haotian Liu and Shanwen Wang and Hongteng Xu},
year={2025},
eprint={2501.13959},
archivePrefix={arXiv},
primaryClass={cs.CL},
url={https://arxiv.org/abs/2501.13959},
}