模型 / Lean Finder (delta-lab-ai)

Lean Finder (delta-lab-ai)

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

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

社区实测

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

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

Lean Finder: Semantic Search for Mathlib That Understands User Intents | OpenReviewLean 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

本形态 ~4.9GB 4-bit · 国内 需代理 · 213 下载

仅 safetensors · 无 pickle 加载风险

快速上手

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

本形态源 ↗

下载动量

30天下载 47 → 102

观测时间线