标签: Lean
清除筛选
Claude 用 11 天写完费马大定理的 Lean 证明：1300 万行、三道机器验证
9 月 4 日，Anthropic 宣布完成费马大定理的首个完整机器验证证明：Claude 在 11 天里以近乎自主的方式写出 1300 万行 Lean 代码，途中证明了 30,300 条定理，最终证明引用其中 29,500 条。整个证明只依赖 Lean 证明助手的三个标准公理，先后经过官方校验工具与一个独立 Rust 内核的全量检查。帝国理工学院的 Kev…
陶哲轩推出 Palomar：Lean 验证数学注册表开放
2026 年 8 月 18 日，陶哲轩（Terence Tao）在个人博客宣布，Lean 验证数学注册表 Palomar 正式开放提交。这个由 Lean FRO 与 ICARM 共同孵化的项目，瞄准的是 2026 年以来日益尖锐的一个问题：AI 生成的数学证明数量激增，但确认一个 Lean 仓库真的证明了它声称的结果，对非 Lean 专家来说异常困难。 陶哲…
OpenAI Astra 数学新结果：十项长期问题与 Lean 验证
2026 年 8 月 1 日，OpenAI 公布了一份名为《Ten Advances in Mathematics and Theoretical Computer Science》的论文，介绍内部版本 Astra 在数学和理论计算机科学中的十项新结果。OpenAI 的表述很克制：这些问题至少十年没有出现主要进展，多数问题的开放时间更久。 这份材料的看点不止…
GPT-5.6用一段十页提示词，关闭凸优化30年的复杂性缺口
2026 年 7 月 10 日，OpenAI 在自己的 CDN 上放出一篇 PDF，声称 GPT-5.6 Sol Ultra 用 64 个并行子代理、不到一小时，证明了图论里悬挂了 50 年的 Cycle Double Cover 猜想。数学界在震动与质疑中展开了审阅。六天后，UC Berkeley IEOR 教授 Phillip Kerger 把 Open…