1. 从一则“新闻”说起当AI挑战数学竞赛时我们到底在讨论什么最近一个标题在技术圈和数学爱好者中流传开来“IMO题库‘过时’了OpenAI内部模型挑战最新First Proof做了7天错了一半”。这个标题信息量很大也极具误导性。它巧妙地混合了几个容易引爆焦虑和好奇心的元素代表人类智力巅峰的IMO国际数学奥林匹克竞赛、AI领域的明星公司OpenAI、一个听起来很前沿的“First Proof”概念以及一个戏剧性的结果——“7天错了一半”。这很容易让人产生一种错觉AI已经强大到可以挑战最前沿的数学研究但结果似乎又“翻车”了于是引发了一场关于AI能力边界和人类智慧优越性的讨论。但事实真的如此吗作为一个长期关注AI在推理和形式化验证领域进展的从业者我必须说这个标题更像是一个精心设计的“标题党”。它把几个不同层面、不同语境下的概念强行糅合在一起制造了一个吸引眼球但失真的叙事。要理解这件事的真正意义我们得先拆解这几个关键词。首先IMO题库。这是指历届IMO竞赛的题目集合。这些题目确实是人类青少年数学精英智慧的结晶涉及数论、组合、代数、几何等核心领域以构思精巧、解答需要深刻的洞察力和创造性著称。但说它“过时”是一个不准确的表述。数学真理不会过时IMO题目的价值在于其思维训练而非知识的新旧。AI在解决这类有明确答案的“谜题”上近年来确实取得了长足进步例如DeepMind的AlphaGeometry就在几何题上达到了IMO金牌水平。但这和“过时”无关更像是AI在特定类型问题求解上找到了有效的模式。其次OpenAI内部模型。标题没有指明是哪个模型。是GPT-4是未发布的O1还是专门为形式化数学设计的模型这很重要。OpenAI的研究方向很广从大语言模型到推理模型再到与数学证明相关的项目如之前传闻的“Strawberry”。不同模型的能力天差地别。一个未经证实的“内部模型”测试其参考价值有限。最核心的混淆点在于“最新First Proof”。在数学研究领域“First Proof”通常指一个公开的、未解决的猜想或问题的第一个完整证明。这是一个开创性的工作。我不认为OpenAI会贸然用一个内部模型去挑战一个真正意义上的、悬而未决的数学前沿问题的“First Proof”并公开展示一个“错了一半”的结果。这不符合其研究发布的常规。更可能的情况是这里的“First Proof”指的是某个形式化数学竞赛或基准测试Benchmark中的题目。例如在形式化验证社区有像“MiniF2F”、“IMO-AG-30”这样的数据集也有“ProofNet”这样的基准它们将数学问题包括一些IMO题目转化为形式化语言如Lean Isabelle/HOL要求模型生成能被验证器通过的证明步骤。挑战这些基准更像是让AI学习一种特定的、严格的“编程语言”证明语言而不是进行天马行空的数学创造。所以更合理的解读是OpenAI的研究人员可能用某个内部模型在某个形式化数学证明基准上进行了为期一周的测试结果在部分题目上失败了。这非但不能说明AI“不行”反而揭示了当前AI在数学推理特别是形式化证明这一硬核任务上面临的真实挑战与进展。这才是值得我们深入探讨的技术内核。2. 数学证明AI面前的“珠穆朗玛峰”为什么说数学证明对AI来说是难啃的硬骨头这得从数学证明的本质和当前主流AI大语言模型的工作原理之间的根本性矛盾说起。数学证明追求的是绝对的、逻辑上无懈可击的确定性。从一个公理或前提出发通过一系列严格的逻辑推导规则如演绎推理最终得到结论。每一步都必须清晰、明确且可被独立验证。整个证明链像一座精密的金字塔基石稳固层层递进不容许任何模糊、跳跃或“大概率正确”。而当前主导AI领域的大语言模型LLM其核心能力是基于海量文本数据的概率建模。它通过学习文本中词汇、短语、句子之间的共现概率来预测下一个最可能的词或序列。它的输出是“统计上最合理的文本”而不是“逻辑上必然正确的推导”。LLM可以写出看起来非常像数学证明的文字因为它见过很多证明的“模板”和“套路”。它可以模仿证明的叙述风格使用正确的数学术语甚至能完成一些中等难度的、有标准解法的题目。但是当面对需要深度洞察、创造性构造比如构造一个巧妙的辅助线或反例、或者进行长链条、多步骤的严密推理时LLM的“概率本质”就会暴露短板。这种矛盾具体体现在几个方面幻觉与逻辑跳跃LLM可能会“自信地”写出一个错误的推论或者跳过关键的、非平凡的推导步骤直接给出一个看似合理的结论。在非形式化的文本中这不易察觉但在严格的数学证明中这就是致命的漏洞。缺乏真正的“理解”LLM对数学概念的理解是表面化的、基于文本关联的。它知道“勾股定理”这个词常和“直角三角形”、“a²b²c²”一起出现但它并不“理解”这个定理为什么成立以及它在不同几何情境下的深层含义。这种理解缺失使得它难以灵活运用定理或在全新的问题情境中进行类比和迁移。长程依赖与状态保持复杂的数学证明往往需要维护一个不断演变的“思维状态”定义了哪些变量做了哪些假设已经证明了哪些引理。LLM在处理长文本时容易遗忘或混淆上下文中的关键信息导致证明前后矛盾或循环论证。因此让AI做数学证明尤其是形式化证明相当于要求一个基于统计和模仿的“语言大师”去扮演一个追求绝对理性和逻辑的“逻辑学家”。这无疑是当前AI面临的最严峻挑战之一也是衡量AI是否具备“真正智能”的关键试金石。3. 形式化证明为AI搭建的“脚手架”与“裁判”既然大语言模型直接生成自然语言证明不靠谱研究人员就想到了一个办法形式化证明Formal Proof。这是将数学证明“降维”到AI更容易处理层面的一种策略可以看作是为AI攀登数学高峰搭建的“脚手架”并引入了一个铁面无私的“裁判”。什么是形式化证明简单说就是用一种定义极其严格、毫无歧义的计算机语言形式化语言如Lean, Coq, Isabelle/HOL来书写数学定义、定理和证明。在这种语言里每一个数学对象如数字、集合、函数都有精确的类型定义每一个推理步骤如“因为A所以B”都必须对应一个该语言内置的、被验证过的推理规则。整个证明过程最终会转化为一系列计算机可以逐条检查的指令。这个过程如何帮助AI提供了明确的“游戏规则”对于AI模型来说形式化语言就像一个语法和语义都极度受限的“编程语言”。模型的任务不再是生成一段自由、模糊的自然语言而是生成一串符合该语言语法、并且能通过类型检查器和定理证明器验证的代码。这大大缩小了搜索空间让问题变得更结构化。引入了即时、绝对的反馈这是最关键的一点。在自然语言证明中判断对错需要人类专家审阅耗时且主观。在形式化证明中写完一步立刻可以运行验证器如Lean的#check或lean --run。如果验证通过计算机说“True”如果不通过计算机会明确报错指出在哪一行、哪个类型不匹配或哪个引理未找到。这为AI训练提供了完美的强化学习信号。模型可以尝试不同的证明步骤根据验证器的反馈奖励或惩罚来调整自己的策略。创造了丰富的训练数据像MathlibLean的大型数学库这样的项目积累了数以百万计的形式化定理和证明。这些数据是结构化的、机器可读的、且被验证正确的。它们成为了训练“数学证明AI”的优质语料。模型可以学习从定理陈述Goal到证明脚本Tactic的映射关系。所以当我们看到“OpenAI内部模型挑战First Proof”的消息时几乎可以肯定它挑战的是一个形式化证明基准中的题目。模型的工作流程可能是接收一个用形式化语言表述的定理Goal然后自动生成一系列证明指令Tactic试图让验证器输出“证明完成”。所谓的“做了7天错了一半”很可能是指在某个包含若干题目的测试集上经过一段时间的运行可能是多轮尝试、搜索只有大约一半的题目被成功证明。4. 剖析“7天错一半”可能的技术路径与真实瓶颈那么一个AI模型是如何尝试解决一道形式化证明题的呢结合当前领域的研究我们可以推测几种主流技术路径并分析“错了一半”背后可能的原因。4.1 主流技术路径猜想检索增强生成RAG与定理库调用这是最直观的方法。模型会将当前要证明的定理Goal与形式化数学库如Mathlib中已有的定理进行相似度匹配检索出可能相关的定理、定义和已有的证明片段。然后它尝试将这些“零件”组合起来构建证明。这就像是一个拥有超强记忆力的助手能快速从海量工具书中找到可能用得上的工具。但对于需要创造性组合或全新构造的题目仅仅检索和拼接是远远不够的。基于强化学习的策略搜索将证明过程建模为一个马尔可夫决策过程MDP。状态State当前未证明的目标集合通常是一个目标栈。动作Action应用一个合法的证明策略Tactic如intro h引入假设,apply theorem_name应用某个定理,rewrite [eq]重写等式等。奖励Reward成功证明整个命题获得1奖励证明失败或进入死胡同获得0或负奖励。 模型作为智能体通过不断尝试不同的动作序列证明步骤根据最终是否证明成功来更新其策略网络。这种方法能探索更广阔的证明空间但搜索成本极高需要大量的计算和环境交互即运行验证器。“7天”这个时间可能就花在了这种大规模的搜索和试错上。监督微调与思维链CoT使用大量“定理-证明”对数据对基础大语言模型如GPT-4进行微调使其学会生成形式化证明语言。同时借鉴自然语言推理中的“思维链”技术让模型在生成最终的形式化代码前先以自然语言或中间形式“思考”证明思路。这有助于模型规划证明的整体结构再将结构分解为具体的形式化步骤。OpenAI的O1系列模型就被认为强化了这类逐步推理的能力。符号推理与神经符号结合纯神经模型LLM擅长模糊匹配和模式识别但在符号逻辑操作上较弱。因此一些研究尝试将神经模型与传统的符号推理引擎如自动定理证明器结合。神经模型负责提出证明方向、选择有用的引理符号引擎负责执行精确的逻辑推导和验证。两者协同可能比单一方法更强大。4.2 “错了一半”的潜在原因分析即使采用了上述先进技术在复杂的证明题面前AI依然会折戟。原因可能包括搜索空间爆炸对于一道中等难度的题可能的证明路径组合是一个天文数字。即使使用启发式搜索和强化学习在有限的计算资源和时间内如7天也可能无法穷尽或找到那条正确的路径。缺乏高层规划能力模型可能擅长执行局部的、战术性的推理步骤但缺乏对整体证明战略的宏观规划。比如它不知道应该先证明一个关键的引理或者使用反证法、数学归纳法等高层策略。这导致它在证明的“迷宫”里盲目打转。形式化语言本身的复杂性Lean等语言虽然精确但学习曲线陡峭。模型需要精确掌握大量库函数、定理的名称和调用方式。一个细微的语法错误或类型不匹配就会导致整个证明失败。这要求模型具备近乎完美的代码生成能力。训练数据的局限尽管Mathlib等库很大但它覆盖的数学领域和问题类型仍然是有限的。如果测试题目涉及的知识点或证明风格在训练数据中不常见模型的性能就会大幅下降。这解释了为什么在“最新”的基准上表现不佳——模型没见过类似的东西。评估标准的严苛性在形式化证明中没有“部分正确”。证明要么完全通过验证要么失败。模型可能生成了99%正确的证明但因为最后一步的一个小错误就被判定为全错。这种“二进制”评估标准非常残酷。“做了7天错了一半”这个结果如果属实恰恰生动地说明了当前AI在形式化推理上的现状有进展能解决一部分问题但远未达到可靠和通用的程度。它更像一个在特定规则下刻苦练习的学生在一些模拟考中取得了不错成绩但面对真正新颖、复杂的考题时仍然会力不从心。5. 超越标题AI数学研究的真实价值与未来方向我们不应该被“挑战IMO”、“First Proof”这类吸引眼球的词汇带偏。AI在数学领域的应用其真实价值远不止于“做题”或“竞赛”。它正在悄然改变数学研究本身的工作方式。数学家的“超级辅助”这是目前最现实、也最有效的应用。AI可以帮数学家完成那些繁琐、耗时的“体力活”。例如文献检索与归纳快速从海量论文中找到与当前研究相关的定理、引理和证明思路。猜想生成通过分析大量数学结构的数据发现数据中隐藏的模式或关系提出可能成立的新猜想供数学家去严格证明。这已经有一些成功的案例。证明细节填充数学家提出一个证明的宏观思路草图AI可以尝试将这个思路转化为详细的形式化证明步骤或者帮助检查证明中是否存在细微的漏洞。公式化简与计算处理复杂的符号计算和代数化简。形式化验证的普及者随着Mathlib这类项目的发展将经典数学知识形式化入库本身就是一个巨大的工程。AI可以加速这个过程自动或半自动地将教科书中的证明转化为形式化代码。这不仅能构建一个前所未有的、机器可读的精确数学知识库也为未来所有基于数学的工程如芯片设计、航天软件、加密协议提供了最高级别的正确性保障基础。教育领域的个性化工具AI可以根据学生的学习情况生成不同难度的数学习题并提供个性化的解题指导和步骤反馈。在形式化证明的辅助下它甚至能精确指出学生证明中的逻辑错误所在而不仅仅是答案对错。未来的发展方向可能集中在更好的推理架构开发专为推理设计的新型模型架构超越传统的自回归下一个词预测范式。例如更显式地建模状态、规划和回溯机制。混合智能系统更深度地融合神经网络的直觉、模式识别能力与符号系统的逻辑、精确性。让人数学家在高层战略上引导AI在底层战术上执行和探索。更大规模、更多样化的训练数据持续扩充形式化数学库并探索如何将非形式化的数学文本教科书、论文与形式化代码更好地关联起来训练模型。交互式证明助理的智能化将AI深度集成到像Lean、Coq这样的交互式定理证明器中使其能理解用户的意图主动提供证明建议实现真正的“人机协同证明”。回到那个标题它或许用一个夸张的叙事吸引了我们但它指向的趋势是真实的AI正在以前所未有的方式介入严谨的逻辑推理领域。它的表现可能时而令人惊艳时而显得笨拙但这正是技术探索的常态。我们关注的焦点不应是“AI能否打败人类数学家”这种二元对立的问题而应是“AI如何成为数学家乃至所有需要逻辑思考者的强大盟友”以及“我们如何利用这项技术去探索那些曾经因为过于复杂而无法触及的数学深空”。这条路很长“7天错了一半”只是一个路标它告诉我们山很高路很陡但攀登的过程本身就在拓展着智能的边界。