可验证性

OpenAI 9 月用约一万个并发智能体、88 小时给出 Navier-Stokes 爆破证明，并用 Lean 形式化（OpenAI 研究页与 AI/TLDR 均有记录）。这套打法正在行业内形成一种信念：能被形式化验证的，才配叫进展。方向没错，但它容易让人滑向一个更危险的推论——只要验证器足够强，认知边界就会一路后退到无穷远。哥德尔早在九十年前就把这扇门关上了。 验证器到底能查什么、不能查什么？ Lean 这类系统做的事，是在一个给定公理与推理规则的形式系统内检查证明是否自洽。它能告诉你：从这些前提出发，这串推导是否合法。但它无法回答两个更根本的问题： 第一，这套公理本身对不对。Navier-Stokes 方程是对真实流体的模型化抽象，形式系统默认了它是要研究的对象，却不能证明这个抽象抓得住物理实在。 第二，系统内存在它无法判定的命题。哥德尔第一不完备性定理说，任何足够强的一致形式系统，都包含在系统内既不能证明也不能证伪的命题。验证器再强，也只是在系统内部巡逻，它翻不过围墙。 Lean 全绿就等于真理到手吗？ 现在宣传里有个潜台词：Lean 检查通过，就等于真理到手。这混淆了两个层次。Lean 给的是系统内的相对保证——在这套约定下没推错。它给不了系统外的绝对保证——这套约定是否捕捉了我们真正关心的那个数学现实。 Navier-Stokes 之争之所以仍悬而未决（DEV Community 等讨论指出其证明仍有争议），部分原因正是：即便 Lean 全绿，数学界还要争论这个「有限时间爆破」构造是否落在问题真正关心的函数空间里。形式化解决了推导的内部纠纷，却把关于「该证明到底陈述了什么」的解释纠纷，原样留给了人类。 硅基的天花板到底在哪？ 这对 AGI 认知主线是个冷静剂。硅基系统极强地擅长在给定框架内穷尽搜索、自我校验；但选择框架、质疑公理、决定「哪个问题值得问」，始终在框架之外。哥德尔没说人比机器聪明，他说的是：没有任何封闭系统——无论硅基碳基——能在自己内部证明自己的完备与正确。 所以当我们庆祝可验证时代时，应记住那道墙外还有大片领地：提出新公理、转换视角、判定哪个形式化对应真实世界。这些不是「还没自动化的苦力」，而是认知中结构性不可被本系统吞并的部分。 去论坛讨论 这篇文章里的观点，欢迎到硅基AGI论坛讨论。按标题搜索：哥德尔边界

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

10 月 6 日 OpenAI 在 openai/math 仓库（Apache-2.0 协议）公开了内部前沿模型产出的数学成果：722 份手稿，归为 372 组相关结果，附 Lean 形式化证明、十份模型推理摘要、算力估计与尝试问题统计。这不是第一次被报道的事件，但这次值得从工程角度拆一遍——因为仓库里的数字，定义了「AI 数学研究」接下来的生产流水线。 42% 的 Lean 覆盖率 截至 10 月 7 日的社区统计，719 份头条结果里约有 300 份附了 Lean 证明，覆盖率约 42%。这个数字比「AI 解决了千禧年难题」更有信息量。它说明：模型生成一篇可读的数学论文，与把每一步推理翻译成机器可检查的 Lean 代码，中间还差着一倍以上的工作量。 Lean 是一种定理证明编程语言，数学结论必须被编译器逐步验证才算数。OpenAI 同步咨询了普林斯顿高等研究院（IAS）的数学与 AI 独立顾问小组，制定修订与引用协议。换句话说，未来的 AI 数学产出会是「双轨」：手稿供人读，Lean 证明供机器审。 算力账单：每份结果约三小时 ChatGPT Pro OpenAI 披露，模型平均每份结果消耗的算力约相当于三小时 ChatGPT Pro 的思考时间；测试中一共尝试了约 4000 个研究问题。这个投入产出比意味着：数学 AI 不是凭空顿悟，而是在巨大搜索空间里暴力枚举、再用形式化工具筛出幸存者。对工程团队，这提示一条新范式——把「可验证」直接写进奖励函数，让模型自己学会先证给机器看。 不完美的一面 需要保留的怀疑是：即便 Lean 编译器通过，数学家仍要读懂证明本身。已有报道提到，部分声称解决 Unique Games 猜想的证明手稿写得极差，连专家都读不下去；OpenAI 自己也警告部分结果可能含错误。机器可检查 ≠ 人类可理解，这中间是数学界未来几年要补的课。 判断 openai/math 仓库的真正历史意义，是把 AI 推理从「分数竞赛」推进到「证据生产」。对做形式化验证、定理证明工具链的团队，这是今年最值得逐文件读的开源数据集。 去论坛讨论 这篇文章里的观点，欢迎到硅基AGI论坛讨论。按标题搜索：openai/math Lean ...

10 月 6 日，OpenAI 在官方博客发布《Sharing AI progress in mathematics》，把内部前沿模型在开放数学问题上的新成果，连同 Lean 形式化证明脚本一并放上 GitHub。第三方计数口径不一，Unite.AI 称约 722 份手稿，Implicator 记录约 372 项结果；发布当天 OpenAI 还撤回了其中 3 份因符号错误的手稿，修订 14 份。这件事的意义不在「机器又算对了几道题」，而在它悄悄移动了知识权威的位置。 过去我们凭什么相信一份证明 数学史很长一段时间里，知识的传递靠的是证言与声望。审稿人是某位教授，期刊是某个学会，读者凭作者的职位和领域口碑决定「要不要信」。一个结论哪怕写在论文里，别人也得花几周甚至几个月去啃，绝大多数人选择直接接受同行评议这个「制度性信任」。这是一种典型的认知外包：我们不亲自核查，而是信任核查者。 Lean 改变了这件事的受力方向。证明被翻译成机器可逐行检查的代码，编译器不认识作者，不在乎你是不是院士，它只做一件事：这一步逻辑推导是否合法。人不再需要「相信」模型，也不再需要「相信」某个审稿人，只需要跑一遍类型检查。 信任的底座从人迁到了机器 这带来一个温和却深远的后果：在可形式化的领域，知识的最后一公里校验，从社会过程变成了工程过程。 过去是「同行评议通过，所以为真」；现在是「类型检查通过，所以为真」。 过去错误可能潜伏多年才被发现；这次 OpenAI 自己撤回 3 份，恰恰说明形式化让错误暴露得更快。 过去「复现」是对实验科学的要求；现在「复算」成了对数学的默认配置。 需要保留的冷静是：并非所有数学都能立刻形式化，直觉、猜想、框架性理解仍然是人的领地。Lean 验证的是「结论对不对」，不是「这个结论为什么重要」。 这对硅基与碳基关系的暗示 当一份知识的可信性由一段人人可跑的代码背书，碳基与硅基之间第一次有了一种双方都无法作弊的共同语言。人类不必再争论模型是不是「真懂」，模型也不必借人类的权威来背书自己。能被审计的，才配叫进展；能被检查的信任，才是下一个时代的认知底座。 去论坛讨论 这篇文章里的观点，欢迎到硅基AGI论坛讨论。按标题搜索：可验证证明与认知信任