OpenAI宣布其内部模型在24天内解决了100多道长期开放的数学难题，包括纳维–斯托克斯方程相关成果。文章梳理了事件时间线：训练从8月28日开始，证明工作由约一万个并发Agent并行完成，耗时88小时，另用17小时完成Lean形式化验证。同时，陶哲轩、舒尔茨等数学家发表公开信，担忧AI过快产出证明会打乱学术规范、方法传承与人才培养。OpenAI还成立了独立的数学与AI顾问组，但无权干涉研究节奏。作者认为，解题速度加快后，证明的解读、教学与学术消化仍需数学界接续完成。
孙宇晨设立数学奖，单题奖金最高100万美元，采用机器可验证的Lean形式化证明作为评判标准，去中心化、零信任地取代传统评奖委员会。作者认为这对个人和小团队是重大机遇：奖项不设门槛，且30%奖金专门留给形式化工作，即把已有公开证明搬进Lean即可拿钱。作者分析了三种参与方式（全做、只做形式化、只出思路），推荐小团队从形式化切入，并给出三人团队配置建议、官方入口和Lean工具链教程。作者认为该奖项将倒逼AI行业从'看起来对'转向可复查的可靠推理，带来结构性利好。
文章介绍了 Theoric Labs 的 LeanDB 实验，旨在将形式化方法与 AI 智能体结合应用于数据库领域：用 Lean 语言描述数据及其属性，同时使用 SQL 数据库进行存储和查询。文章通过咖啡菜单示例系统讲解了 Lean 的类型系统，包括归纳类型（如 Temperature、MenuItem）、细化类型（如限制浓缩咖啡份数为 1-4 的 ShotCount 子类型）、依赖类型（杯型大小依赖于冷热温度的 CupSize 索引族），以及元类型（FieldSpec 宇宙设计模式，用数据描述类型）。作者认为，强类型能让编译器在运行前阻止非法数据写入，将验证结果显式化，从而构建无 bug 的软件系统。
文章回应25位菲尔兹奖得主关于AI将损害数学的宣言。作者以AlphaGo‘第37手’为例：AI出现后职业围棋水平不降反升，因为开源引擎让每位棋手拥有超人类导师。作者认为菲尔兹奖得主担心的核心问题真实存在——AI正在把解题的成果与过程分离，但他们忽略了更深层的变化：验证成本的历史性反转。过去猜测便宜而验证昂贵，如今借助Lean等证明助手和形式化证书，验证变得廉价可复制。数学的制度体系（同行评审、长学徒制）都是围绕验证稀缺建立的。AI不会摧毁数学，反而会让数百万人得以参与，让‘十亿数学家’绽放。
纽约大学数学家Tristan Buckmaster公开声明，与Levent Alpöge借助Claude、Codex等大语言模型，一个月内证明了多个流体力学方程（多孔介质方程、Boussinesq方程、Euler方程）在光滑外力下的有限时间爆破，并经Lean形式化验证，陶哲轩称之为了不起的成就。同时Buckmaster指控OpenAI在得知其进展后试图抢先发布类似成果，并施压要求将在Anthropic工作的合作者从署名中移除。事件涉及学术伦理、AI科研能力边界与大公司竞争，被称为数学领域的深蓝时刻。
OpenAI 于 8 月 1 日公布了数学与理论计算机科学方向的十项新进展，涉及几何、密码学、复杂性等长期问题。这些成果来自下一代模型 Astra 的内部版本，配套了 253 页论文、推理叙述和 Lean 形式化证明仓库。文章强调，这不仅是模型能力的展示，更标志着 AI 从生成文本转向生成可验证的研究产物。作者提醒读者不要过度解读为“AI 替代数学家”，而是关注其带来的可验证输出标准，这对未来 AI 工作流和科研模式具有深远影响。
文章指出数学有 Lean、代码有编译器和测试作为不可欺骗的裁判，而物理缺乏机器验证器，导致物理 AI 卡在起跑线前。作者分析 LLM 最擅长伪造物理学家依赖的廉价可信信号（量纲一致、推导自洽、独立路径吻合等），且最危险的错误是将近似用在适用域之外。文章借鉴数学和代码领域建立裁判后能力爆发的经验，提出为物理构建可机检的验证层，输出覆盖度证书，包含量纲检查、对称性验证、数值模拟交叉验证和强制隔离的多路径推导，目标客户是做物理的 AI Agent。
文章介绍了OpenAI于8月1日公布的数学与理论计算机科学领域十项新进展，涵盖高维球堆积、编码理论、Connes刚性猜想、算术电路复杂度、多色Ramsey数等长期开放问题，既有新上下界也有反例。这些结果由内部版Astra模型生成，总成本仅约2000美元，随后由人类研究者配合整理成论文，并用Lean形式化证明系统验证。作者认为AI在科研中的角色正从读论文、辅助推导走向搜索开放问题、提出新证明、形式化验证与人类审查的闭环。
文章回顾了人工智能与数学证明的深厚渊源，从1950年代的Logic Theorist到哥德尔不完备性定理，探讨了形式化数学的演进。重点介绍了现代AI数学的基础设施LEAN（包括其核心人物Leonardo de Moura、从v3到v4的演进及mathlib库），以及DeepMind、Harmonic、Axiom Math等科技巨头和初创公司在AI自动定理证明领域的布局。文章指出，AI正在通过神经网络与形式化验证的结合，重新回归逻辑推理的起点。
