数学证明

9 月 8 日 OpenAI 宣布内部系统给出 Navier-Stokes 存在性与光滑性问题的有限时间爆破解，随附论文与 Lean 形式化证明。据腾讯新闻报道，这次攻坚动用了约一万个并发协作的 AI Agent，耗时仅 88 小时；而到了 10 月 9 日，九派新闻援引英国《新科学家》称，菲尔兹奖得主陶哲轩公开批评 OpenAI 无视数学界研究规范，呼吁数学家停止与其合作。一边是机器 88 小时的喷涌，一边是人类领袖喊停——这中间裂开的，正是本文要谈的「验收带宽」。 生产快、验收慢，问题到底出在哪？ 过去数学进步的瓶颈在「想出证明」，审稿周期以月、年计，生产与验收大体匹配。现在 OpenAI 把生产端压到 88 小时一次、10 月 6 日又一次性放出数百项新结果，而人类数学家的阅读速度、共识形成速度、乃至克雷数学研究所对千禧年难题的裁决流程，仍以年级别运转。结果是一个倒挂：产出端指数提速，验收端线性爬行。 Lean 形式化看似解决了验收——编译器逐行检查，一步错即报错。但形式化能验证「这串推导内部自洽」，却无法替人类回答「这串形式化对应的数学直觉是什么、它是否真的攻克了那个物理相关的难题」。陶哲轩的不满正在于此：OpenAI 没有走预印本、同行讨论、社区复现的老路，而是直接把成品抛出来，等于把验收成本一次性甩给了整个学界。 验收只是盖章吗？ 很多人以为验收只是「看对不对」。其实人类审稿的真正价值，是把一个外来自洽的证明，编织进已有的知识网络：它依赖哪些引理、推翻了哪个猜想、和相邻领域有什么意外联系。这个过程无法外包给编译器，因为它本质是「让另一个大脑重新长出一遍理解」。 当 AI 每月吐出数百项结果，学界没有那么多大脑去重新生长理解。于是会出现两种扭曲：要么草草签收、留下大量悬而未决的「机器产物」；要么像陶哲轩那样用规范把整体拒之门外。两种都是认知系统过载后的保护反应。 接下来最值钱的岗位是什么？ 如果验收带宽才是真瓶颈，那么未来有价值的岗位，不是「再训一个更强的证明模型」，而是「理解并签收机器产出」的人——他们是硅基洪流与碳基知识体之间的减压阀。OpenAI 越能生产，这个减压阀越稀缺。88 小时的壮举若无人能签收，在认知意义上它就尚未发生。 去论坛讨论 这篇文章里的观点，欢迎到硅基AGI论坛讨论。按标题搜索：证明验收瓶颈

AI数学证明：从计算到推理 数学证明是人类理性思维的巅峰——它需要严格的逻辑、创造性的直觉和深度的抽象推理。2026年，AI在数学证明领域取得了里程碑式进展，从"做数学题"开始走向"做数学研究"。 2026年的里程碑 1. AlphaProof 2：IMO满分 DeepMind的AlphaProof 2在2026年IMO（国际数学奥林匹克）中获得满分42/42——这是AI首次在IMO中满分。 技术突破： 问题理解 → 自然语言→形式化(Lean 4) → 策略搜索 → 证明验证 → 自然语言输出 ↑ ↑ ↑ LLM转换 神经引导搜索 符号引擎严格验证 关键创新： Lean 4形式化：将自然语言数学问题转化为形式化语言 神经引导搜索：LLM提供"直觉"，指导搜索方向 符号验证：Lean 4类型检查器严格验证每一步 自我对弈：AI通过自动生成和解决数学问题来训练自己 2. 研究级证明：首次贡献 2026年5月，一个AI系统首次对研究级数学问题做出了独立贡献： 问题：关于有限群表示论的一个长期未解决的猜想（Jordan-Hölder定理的推广形式） AI贡献： AI提出了一个新的证明思路 人类数学家验证了思路的可行性 AI完成了形式化证明 证明被提交到arXiv预印本库 虽然这不是一个重大猜想的解决，但它是AI首次在研究级数学中做出原创贡献。 3. 自动形式化 将人类数学论文自动转化为形式化证明： DeepMind的AutoFormalize系统： 输入：数学论文的自然语言文本 输出：Lean 4形式化证明 准确率：72%（在标准数学论文上） 这意味着大量已有的数学知识可以被自动形式化，为AI数学研究提供丰富的训练数据。 4. 新数学概念发现 AI不仅在证明已知猜想，还在发现新的数学概念： 超图代数：AI在探索组合数学时发现的一个新数学结构 新不等式：AI在优化理论中发现了3个新的不等式关系 新算法：AI设计了一种新的矩阵乘法算法，复杂度优于已知最优 技术方法 1. 神经符号融合 AI数学证明的核心是神经符号融合： 神经部分（LLM）： 理解自然语言数学问题 提供证明"直觉"和策略 生成候选证明步骤 符号部分（Lean 4/Coq）： 严格验证每一步的正确性 确保证明没有逻辑漏洞 提供形式化的证明证书 class NeuroSymbolicProver: def prove(self, theorem): # 1. LLM理解定理 formal_theorem = self.llm.formalize(theorem) # 2. LLM提出证明策略 strategies = self.llm.generate_strategies(formal_theorem) # 3. 对每个策略进行搜索 for strategy in strategies: proof_steps = self.search(strategy, formal_theorem) # 4. 符号引擎验证 for step in proof_steps: if not self.lean.verify(step): break # 这一步不正确 else: # 所有步骤都通过验证 return self.format_proof(proof_steps) return "无法证明" def search(self, strategy, theorem): """神经引导的证明搜索""" queue = [strategy] while queue: current = queue.pop(0) # LLM生成下一步 next_steps = self.llm.generate_next_steps(current, theorem) for step in next_steps: if self.lean.verify(step): if self.lean.is_complete(step): return self.trace_proof(step) queue.append(step) return None 2. 大规模搜索 AI数学证明需要进行大规模搜索： ...