Prove2Me 走红:支撑 Anthropic 形式化费马大定理的众包平台
burny_tech · x · 2026-09-06
量化研究者 Henry 细讲了 Prove2Me——正是它支撑了 Anthropic 对费马大定理的 Lean 形式化工作,并分享了它源于一门他本不该教的课程的起源故事。
- Prove2Me 是一个数学形式化众包平台:把论文或教科书中的结论拆解成小的 Lean 4 命题(mission),任何人都可以认领验证,也支持把自己的论文提交为待验证任务
- 平台为 AI agent 提供了专门入口(抓取 start.md 即可让 agent 接入参与形式化),示例任务包括马尔可夫链中心极限定理等较深的结果,已有 149 条定理、16 位活跃用户
- 作者强调这体现了「数学形式化规模化」的方向:人工 + agent 协作地把经典定理库持续形式化
「研究」频道最新
- 斯坦福 cs336 课程致谢 NoPE 位置编码研究 — xhluca · 2026-09-06
- 1.5B 小模型实测：来源分级验证让本地 Agent 不再「自信地错」 — UzairArain554 · 2026-09-06
- MasonKamb 抛争议观点：梯度下降是 LLM 与人类认知分歧的原罪 — _arohan_ · 2026-09-06
- Chris Potts 讲解隐学习与可解释性:IPAM 研讨会演讲开放观看 — ChrisGPotts · 2026-09-06
- arXiv 论文:单一指标评估 LLM 鲁棒性会误导,需多层级分析 — burny_tech · 2026-09-06
- 因果基础模型来了:预训练一次,上下文学习估算因果效应 — burny_tech · 2026-09-06