陶哲轩推出 Palomar：Lean 验证数学注册表开放
2026 年 8 月 18 日，陶哲轩（Terence Tao）在个人博客宣布，Lean 验证数学注册表 Palomar 正式开放提交。这个由 Lean FRO 与 ICARM 共同孵化的项目，瞄准的是 2026 年以来日益尖锐的一个问题：AI 生成的数学证明数量激增，但确认一个 Lean 仓库真的证明了它声称的结果，对非 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…