引子

2026年5月，Google DeepMind发布AlphaProof Nexus，一次性解决了9道悬置多年的Erdős开放问题，其中2道已困扰学界长达56年。同年7月，OpenAI的GPT-5.6 Sol Ultra在不到一小时内，成功证明了困扰图论领域长达50年的“循环双覆盖猜想”。64个AI智能体并行探索不同路径——代数视角、结构归纳法、流场表述、嵌入法、极端参数法——并设置了专门的“纠察队”机制，让一部分智能体扮演“杠精”，疯狂攻击每一个被提出的候选证明，只有被严格纠错还能活下来的证明才有资格进入下一轮。

2026年菲尔兹奖颁奖现场，陶哲轩说了一句话：“一个猜想是不是真的，和你希不希望它是真的，是两回事。”但他紧接着提出了一个更让人不安的工作假设：“请全场观众暂时假设，AI很快就能以合理的成本和质量，完成相当比例的研究级数学任务。”

这不是预言，这是一个条件分析。他要求数学家们先假装AI已经赢了，然后问：如果解题这件事AI也能干，那数学家存在的意义是什么？

构造学论要追问的是：当AI的“智能”在数学证明这个最硬的测试场上超越了人类，数学中还剩下什么是AI无法触及的？如果“智能”可以被外部系统复制甚至超越，人类最终的保有量是什么？是思想吗？如果思想也可以被生成，那还剩下什么？

一、智能的边界：AI已经能做什么

先看清事实。

2024年，DeepMind的AlphaProof与AlphaGeometry 2合作，在国际数学奥林匹克竞赛（IMO）模拟测试中达到银牌水平。2025年11月，AlphaProof正式推出，基于形式化语言Lean和强化学习技术，专为证明复杂数学命题而设计。

2026年1月，GPT-5.2 Pro独立证明了一道埃尔德什猜想（#281号，由Erdős与Graham于1980年共同提出），论证过程经陶哲轩验证成立，被评价为“迄今为止最明确的第一类结果（AI主要贡献）”。陶哲轩的评论是：“让我更惊讶的是它避免了错误，比如极限交换或量词顺序的失误，这正是这道题最容易踩的坑。前几代大语言模型几乎肯定会在这些微妙之处栽跟头。”

2026年5月，AlphaProof Nexus在353个开放的Erdős问题中解决了9个，其中2个已悬而未决56年；还在OEIS的492个开放猜想中证明了44个。每个问题的推理成本仅数百美元。

2026年7月，GPT-5.6 Sol Ultra用64个并发智能体，在一小时内产出了循环双覆盖猜想的完整证明。这个猜想半个世纪以来只有“附加条件下成立”的局部结果，完整证明始终无人完成。

这些不是“辅助工具”的成绩。这些是独立完成的、研究级的、经过形式化验证的数学证明。AI已经跨越了从“解题”到“研究”的门槛。

二、思想与智能的构造学区分

在构造学论的框架中，“智能”与“思想”是两个不同的构造层级。

智能是在给定的约束条件下，以最高效率找到从起点到终点的路径。AI的证明生成就是智能的典型表现——给定一个猜想（终点）和一套公理系统（起点和路径规则），AI能在搜索空间中快速找到一条可行路径。AlphaProof Nexus的64个智能体并行探索不同策略、互相攻击、筛选幸存者——这是智能在搜索空间中的高效率运作。

思想是重新定义“什么算作起点”和“什么算作终点”的能力。

庞加莱提出他的猜想时，他做的不是“解题”。他在拓扑学的边界上识别出了一个此前未被识别的位置——一个尚未被命名的缺口，并把这个缺口用精确的数学语言表述了出来。他把它“放置”在了系统的可见区域中。猜想的提出本身，就是一种思想行为。

佩雷尔曼证明庞加莱猜想时，他做的也不是“在给定路径中找到最短路线”。他在拓扑学与微分几何之间铺设了一条此前不存在的通道——把里奇流这个微分几何的工具，翻译成了拓扑学的问题求解语言。这条通道的铺设，改变了两个领域之间的连通性。

智能在给定的棋盘上找最优解。思想在棋盘之外重新画线，改变棋盘的形状。

三、思想的生成：AI能“提出”猜想吗？

AI能“提出”猜想吗？

目前，AI生成猜想的方式主要是模式识别——在海量数据中发现未被注意的规律性，然后将其表述为一个待证明的命题。这种方法可以生成大量候选猜想，其中一部分可能是有效的。AlphaProof Nexus在OEIS中证明了44个开放猜想，这些猜想本身就是人类或AI之前提出的。

但“提出一个有价值的猜想”和“生成一个可验证的命题”之间，存在一个构造学上的差异。

一个有价值的猜想，不仅仅是“一个尚未被证明的命题”。它是一个在系统的边界上被精准定位的缺口——它告诉后续的构造者“这里有一条路可能通向某个重要的地方”，从而引导构造资源的流向。庞加莱猜想之所以有价值，不是因为它的表述精确（虽然它确实精确），而是因为它标记了一个位置——一个单连通三维流形与三维球面之间的位置——这个位置的填补将改变整个拓扑学的地形图。

AI目前能生成命题，但它不能判断哪个缺口值得被标记。判断“值得”需要一种超出模式识别的东西——需要知道系统的历史、知道哪些方向已经被探索过、知道哪些路径一旦打通将产生最大的结构影响。这种判断依赖于对系统“地形图”的整体感知，而不仅仅是局部的模式匹配。

（待续...）

支持单位：