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

Lean Finder (delta-lab-ai)

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

作者 delta-lab-ai

~4.9GB 4-bit许可 可商用任务 向量嵌入最近核对 2026-07-08
格式
4-bit
文件
~4.3GB
运行内存
~4.9GB–6.4GB
运行时
transformers
下载
213

仅 safetensors · 无 pickle 加载风险

Hugging Face 源仓库 ↗

适合与不适合

入选理由
提供在线试用和论文。
对位
替代现有 Lean 搜索引擎与 GPT-4o 定理检索
适合
查找 mathlib 定理 / 机器辅助证明检索
不适合
通用文本嵌入任务

独立证据与社区反馈

2 个独立来源 · 另 1 官方/转载最近验证 2026-07-08

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

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

可信度ICLR 2026 论文，用户研究中 Top-3 偏好率 81.6%，Recall@1 相对提升 30%+ 对比 GPT-4o

完整规格

规模
8.2B · 下载 ~4.3GB · 显存最低 ~4.9GB · 推荐 ~6.4GB · 4-bit(估算)
授权
Apache-2.0 · 可商用
框架
transformers / sentence-transformers / text-embeddings-inference
维度
4096 维 · 40k 序列
访问提示
Hugging Face 可能需要代理

下载动量

30天下载 50 → 109

观测时间线