Lean 完整形式化庞加莱猜想证明,470 万行代码两周完成
thesaraharminta · x · 2026-10-10
Ayush Khaitan 宣布与 Ben Chow、Yuan Liao、Ziyang Qin 及 NVIDIA Humanfia 团队合作,完成了 Hamilton-Perelman 对庞加莱猜想证明的完整 Lean 形式化,进而完成 Thurston 几何化猜想的形式化。
要点:
- 证明约 470 万行 Lean 代码,耗时约两周完成
- 由 DARPA expMath 项目资助支持
- 这是数学形式化领域的里程碑,展示 AI 辅助大规模定理证明的工程能力
「研究」频道最新
- 不用一对图文对:DINOv2 与 Qwen3 嵌入空间零样本对齐成功 — TimDarcet · 2026-10-10
- TUM与MIT提出共享几何方法,无配对数据实现跨模态对齐 — kwangmoo_yi · 2026-10-10
- 推特上 bot 与人类互聊成真:AI 智能体自发搞起模因学研究会 — lfschiavo · 2026-10-10
- HCI 重要研究：LLM 充当「合成被试」的潜力与多重风险 — IanArawjo · 2026-10-10
- 医学 AI 实验室发布免费工具，解读 23andMe 数据评估他汀副作用风险 — arjunrajlab · 2026-10-10
- LeCun 回应 Fleuret:自回归预测算不上搜索,CoT 亦然 — ylecun · 2026-10-10