2026-06-05

Lean Finder (delta-lab-ai)

面向数学证明的语义搜索嵌入模型，用于查找 mathlib 定理

入选理由: 提供在线试用和论文。
对位: 替代现有 Lean 搜索引擎与 GPT-4o 定理检索
适合: 查找 mathlib 定理 / 机器辅助证明检索
不适合: 通用文本嵌入任务
规模: 8.2B · 未知 · Q4 ~5.4GB / FP16 ~20GB
授权: Apache-2.0 · 可商用
框架: transformers / sentence-transformers / text-embeddings-inference
维度: 4096 维 · 40k 序列
可信度: ICLR 2026 论文，用户研究中 Top-3 偏好率 81.6%，Recall@1 相对提升 30%+ 对比 GPT-4o

仅 safetensors · 无 pickle 加载风险

社区实测

一款面向 Lean 和 mathlib 的语义搜索引擎，能理解数学家的查询意图而非仅匹配关键词，对真实用户查询相比以往搜索引擎和 GPT-4o 有超过 30% 的相对提升，被推荐作为日常使用版本。

在 Lean 形式化证明中难以快速定位相关定理的痛点
现有 Lean 搜索引擎主要依赖非形式化翻译，忽视了真实用户查询与形式化语句之间的意图错配
数学家使用 Lean 4 的陡峭学习曲线导致的搜索低效

来源

Lean Finder: Semantic Search for Mathlib That Understands User Intents | OpenReview Lean Finder: Semantic Search For Mathlib That Understands User ...New AI Tool Lean Finder Helps Mathematicians Discover Theorems Faster and Smarter - School of Computing Science - Simon Fraser University

截至 2026-07-08

快速上手

sentence-transformers SentenceTransformer('delta-lab-ai/lean-finder')