此页是 2026-06-05 的观测快照,查看该模型当前信息 → /m/delta-lab-ai__lean-finder/

归档 / 2026-06-05 / Lean Finder (delta-lab-ai)

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

评分详情

Q1: 今天能接上用吗 5 / 5
Q2: 有可信证据吗 3 / 5
Q3: 是新东西吗 5 / 5
总分: 13

HuggingFace 原始数据 (抓取于 2026-06-05)

作者: delta-lab-ai
任务类型: feature-extraction
推理库: transformers
下载: 213
点赞: 2
许可证: Apache-2.0
标签: transformers, safetensors, qwen3, text-generation, sentence-transformers, sentence-similarity, feature-extraction, text-embeddings-inference, arxiv:2510.15940, license:apache-2.0, endpoints_compatible, region:us

探索