A.I. 日报
OpenAI内部模型产出722篇数学手稿
2026年10月6日，OpenAI发布由未公开发布的内部模型生成的722篇数学手稿，分属372个结果族，涵盖几何、代数、数论等方向，部分结果涉及长期未解问题。许多证明已用Lean形式化验证，次日因符号错误撤下三篇，表明人类核验仍具决定性。
Lean
6 篇报道Lean 是一个交互式定理证明器，用于把数学证明写成计算机可以逐行检查的形式。近期围绕它的报道包括：OpenAI 发布纳维-斯托克斯方程 AI 解答并附 Lean 形式化证明；一项 AI 辅助工作给出 11 个正方形最优堆叠的完整证明，7,920 个 Lean 模块全部通过；Thomas Hales 在陶哲轩博客上讨论 Lean 等证明助手的可靠性；Hacker News 上还有人争论 Lean FRO 用不到 OpenAI 1% 的资源做出了更扎实的基础工作。
相关话题
- OpenAI3
- Rocq2
- ChatGPT1
- Lean FRO1
- Leonardo de Moura1
- Sam Altman1
- Feit-Thompson theorem1
- Fermat's Last Theorem1
- Terence Tao1
- Thomas Hales1
- Mathlib1
- Bend1
HN讨论：数学家为何抛弃OpenAI
Hacker News上一篇文章批评OpenAI在数学领域的做法，认为其靠预算和宣传而非实际贡献占据前沿，信任已破裂。文章称Lean FRO以不到OpenAI 1%的资源做出了更诚实、更有影响力的基础贡献，并指责巨额投入被用于贬低劳动者。作者主张问题不在LLM技术本身，而在于行业行为。
Thomas Hales谈Lean定理证明器的可靠性与AI
数学家Thomas Hales在Terence Tao博客发表客座文章，讨论Lean等证明助手在数学可靠性方面的价值与AI相关隐忧。文章提到四色定理、Feit-Thompson定理、开普勒猜想及今年完成的球填充、Navier-Stokes爆破和费马大定理等重大形式化项目，使形式化验证获得更广泛关注。
AI辅助完成11个正方形最优堆叠证明
一项AI辅助证明给出了11个正方形最优堆叠的完整最优性证明，所有7920个本地Lean模块通过验证且最终审计无遗漏，几何与检查器可靠性仍采用常规Lean证明。
Bend：用证明阻断AI错误的编程语言
Bend 是一门宣称通过内置“法律”(LAWS.bend)与可验证证明(PROOF.bend)防止 AI 引入错误的新语言，编译为原生代码并可在 GPU 上并行运行。其类型检查器兼作证明检查，声称对中等代码库在秒级完成校验，单核接近 C 的速度、GPU 上最高可达百倍加速。该设计旨在让 AI 在提交前必须给出形式化证明以避免回归。
OpenAI 分享 AI 生成的 Navier–Stokes 解与 Lean 形式化证明
OpenAI 分享了一份 AI 生成的 Navier–Stokes 千年难题解答，包含一篇写作说明与在 Lean 中的形式化证明。该材料公开了 AI 在数学问题求解与机器证明方面的应用示例。
已经到底了