多伦多大学数学家Daniel Litt称AI长证明受制于验证能力
多伦多大学数学家Daniel Litt表示，当前AI模型在数学上的关键瓶颈并非生成文字，而是无法可靠验证复杂推导的正确性；模型可以写出证明，却未必知道证明在哪一步失效。
Litt称，向模型索取较短证明后再追问其是否正确，模型常会自行否认或修正先前结论；但证明变得足够长、包含大量定义、引理、分类讨论和引用链后，错误可能被后续文本掩盖，模型也缺乏稳定的全局一致性检查能力。
他提到一份声称解决正特征域奇点消解问题的论文，全文约800页且由AI生成。该问题属于代数几何中的基础难题：目标是在不改变对象双有理结构的条件下，经由一系列操作将奇点转化为光滑结构；在特征零情形已有经典结果，而正特征情形仍包含高难度开放问题。
Litt称自己尚未在这份800页文本中定位具体错误，但认为其不可能已构成有效证明：该结论若成立将是数学重大突破，而既没有人类专家完整审阅，也没有现有模型具备审计整份复杂证明、追踪所有依赖关系并独立确认结论的能力。
该判断与Litt此前对AI数学能力的立场形成反差。他曾就AI能否在2030年前独立写出达到2025年《Annals of Mathematics》水准的数论论文下注，并在AI已展示对部分数学问题的实质性进展后提前承认判断失误；但他仍将“可验证的长链推理”视为从局部解题走向自主数学研究的分界线。
市场机制上，资金会优先流向形式化验证、定理证明器、证明搜索、代码验证、科学计算与高质量训练数据基础设施，而非单纯追逐能输出更长推理文本的模型。受益方包括能将模型生成结果接入Lean、Coq、Isabelle等可机器检查体系的开发者，以及拥有数学、工程和科学验证数据的机构；承压方是将自然语言AI输出直接包装为科研结论、金融模型或安全关键代码结论的产品，因为其责任成本将随着错误难以审计而快速上升。
来源：公开信息
ABAB AI 解读
数学史上，“提出猜想”和“给出可审计证明”一直是两种完全不同的能力。Andrew Wiles在1993年公布费马大定理证明后被发现存在关键缺口，随后与Richard Taylor用近一年时间补全；Grigori Perelman提出Poincaré猜想证明后，数学界也花费多年组织专家核验与整理。Litt的800页例子处在同一逻辑下：长文本不是证明强度的信号，反而提高了局部假设错配、符号漂移、隐含前提遗漏和引理循环引用被漏检的概率。
资本路径正在从“生成能力”转向“验证闭环”。大模型公司可用论文、教材、代码和合成推理轨迹训练模型提出候选证明，但最终产品化需要把候选答案编译到可检查的形式系统中：模型负责搜索、拆分子问题与生成形式化草稿，定理证明器负责判定每一条推导是否满足公理和规则。这个路径与软件工程中GitHub Copilot到静态分析、单元测试、持续集成和形式化验证的演化一致——生成代码的边际成本下降后，测试、审计与责任归属成为稀缺资源。
行业类比最接近AlphaGo到AlphaFold的差异。围棋有明确规则和胜负判定，模型可以通过自我对弈得到高质量反馈；蛋白结构预测则可以用实验结构数据评估，但预测结果仍需实验验证。开放数学介于两者之间：形式化后的命题可由证明内核做二元检验，但把真实数学语言、定义与研究方向完整翻译进形式系统，仍需要昂贵的人类专家工作。当前模型处在“生成候选路线和局部步骤”的扩张阶段，尚未进入“端到端、自动产出并自动认证重大理论”的控制阶段。
本质属于定价权转移。模型把写作、检索和局部推导变成低成本能力后，可信度不再由谁能写出最长的证明决定，而由谁控制验证系统、形式化语言、权威数据集和专家审稿网络决定。生成端的供给会爆炸，验证端的人力、工具和注意力却相对稀缺；因此AI越能快速制造复杂结论，独立核验的成本越高，验证基础设施的价值越可能向少数拥有工具链与标准制定权的平台集中。
ABAB News · 认知定律
能生成答案，不等于能承担答案
信息越廉价，验证越成为稀缺资产
复杂度不是壁垒，可信验证才是壁垒