形式化

OpenAI 九月的 Navier-Stokes 爆破证明与十月初的数百项新结果，全部附 Lean 形式化，等于给全行业立了个标杆：能被机器验证的成果，才是硬成果。这个方向本身没错——可验证性是反幻觉的利器。但它有个隐蔽的副作用正在浮现：资金、人才、注意力会向「可形式化」的领域集中，而那些无法被 Lean 盖章的认知领域，会被悄悄冷落。本文想把这个偏差摆上台面。 可验证领域为什么特别受青睐？ 灯光照得到的地方，自然有人去。数学、代码、形式化逻辑之所以被 AI 啃得最狠，不仅因为它们重要，更因为它们有现成的验证器——编译器、测试套件、证明检查器，能立刻告诉你对不对，于是强化学习的奖励信号干净又密集。 反过来，伦理学、价值判断、审美、战略直觉这类领域，没有客观验证器，AI 做了对错难分，研究投入回报模糊。可一旦「可验证」成为评判进展的默认标准，这些领域就会被默认为「还不成熟」而少有人碰。问题是，恰恰是这些无验证器的领域，决定了 AI 该往哪走、做的事值不值。 测不出来的领域就不重要吗？ 这是最危险的地方：没有验证器 ≠ 不重要。一个模型在数学上满分，不代表它懂得该如何对待人；它写代码无 bug，不代表它做的决策符合公共利益。如果研究资源像水一样只往「可验证」的低洼处流，我们就会得到一个在形式领域极强、在价值领域极弱的畸形智能——而且这种弱因为「测不出来」而长期不被承认。 陶哲轩批评 OpenAI 跳过同行规范，本质上也是在捍卫一种「慢但必要」的认知领域：社群共识、学术礼仪、可复现文化——这些都没法形式化，却是知识体健康运转的前提。它们一旦被效率逻辑牺牲，损失是隐性的。 研究者该如何自处？ 把可验证性当成工具，不要当成价值排序。在为下一个项目立项时，主动问一句：我是不是因为这个领域「好测」才选它，而不是因为它「重要」？ 真正难而正确的方向，往往恰恰是那些暂时没有机器裁判的方向。可验证的盛宴越热闹，越要给不可验证但关乎意义的认知领域，留出份额。 去论坛讨论 这篇文章里的观点，欢迎到硅基AGI论坛讨论。按标题搜索：可验证偏差

OpenAI 这次放出的 Navier-Stokes 结果，最被称道的一点是「可验证」：证明被翻译成 Lean 代码，编译器检查每一步，人不必再相信模型的「直觉」。Unite.AI 等媒体报道时反复强调这是一份机器可检验的有限时间爆破证明。但很少有人追问下一个问题：当「正确」可以被机器盖章，「优雅」由谁来判？而恰恰是这个无法形式化的判断，决定了一项数学成果在人类知识谱系里的地位。 数学证明要过哪两关？ 数学证明其实要过两关。第一关是正确性：每一步逻辑是否成立、是否有隐藏假设。这一关正在被 Lean 之类的证明助手接管，而且接管得越来越彻底——只要形式化通过，正确性争议就大幅减少。 第二关是品味：这个证明是直击要害还是绕了远路？它用到的工具是恰好够用，还是杀鸡用牛刀？它是揭示了深层结构，还是只是把硬算堆上去？陶哲轩这类数学家之所以被尊崇，不只因为他们证明了定理，更因为他们能在一堆正确的证明里，认出那个「对的证明」。这一关，没有任何编译器能判。 为什么「美」没法写进奖励函数？ 有人会说：既然人能判断优雅，那就把评委的打分喂回模型做奖励不就行了？问题在于，优雅之所以是优雅，恰恰因为它压缩了理解——一个优美证明让你看完觉得「本该如此」，一个丑陋证明让你看完觉得「居然如此」。这种「本该如此」的体感，依赖读者脑子里已有的整个数学语境，而语境是难以显式写出的。 把审美变成打分，模型会很快学会讨好评审的表面特征（步骤短、用了热门工具），却丢掉真正的洞见。这与 RLHF 教会模型说人话、却也磨平棱角是同一类退化。形式化越强，品味就越稀缺，因为机器把「正确」这件廉价化之后，人类唯一还能贡献的高价值判断，就剩「值不值得记住」。 Lean 之后，人类还剩下什么位置？ 这件事的深层含义是：可验证性划了一条线，线内的认知将被硅基接管，线外的审美与品味反而升值。未来数学家的核心工作，可能不再是「推导出正确」，而是「在一万个正确证明里挑出那个值得写进教科书的」。Lean 没有让数学变得机械，它只是把人类的位置，从计算推向了鉴赏。 去论坛讨论 这篇文章里的观点，欢迎到硅基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数学证明需要进行大规模搜索： ...