陶哲轩谈AI在数学研究中的错位问题

数学家陶哲轩近日在其个人博客上发表了一篇文章，题为《数学中人工智能的错位》。该文围绕人工智能工具在数学研究中表现出的偏差与错位展开讨论，很快在技术社区引发关注，并出现在开发者聚集的讨论平台上。

所谓错位，指的是AI系统在数学场景中的能力分布与数学研究的真实需求之间存在明显落差。长期以来，外界对AI的期待往往集中在能否解决难题这一单一维度上，但对于真正从事数学研究的人而言，日常工作中占据大量时间的环节并不是攻克某个悬而未决的猜想，而是文献梳理、符号推导、反例构造、证明草稿的形式化整理，以及与同行协作时的表述校准。如果AI工具在这些环节上表现平平，却在个别竞赛式题目上表现亮眼，那么它带来的实际增益就会与宣传中呈现的形象产生偏离。

与此同时，错位也可能出现在另一个方向：AI生成的数学内容表面流畅可信，却可能包含难以察觉的漏洞。数学是一门对严格性要求极高的学科，一个符号的错误、一个隐含前提的缺失，都足以让整个证明失效。对于不熟悉某一细分领域的读者而言，识别这类问题往往需要付出与重新推导相当的成本，这使得看起来省事的工具反而可能增加验证负担。

这种错位对AI开发者而言具有直接的工程意义。要让模型在数学领域真正可用，仅靠扩大参数规模或增加训练数据并不足够，还需要在可验证性上做文章。形式化证明语言提供了一条可行路径：把推理过程翻译成机器能够逐步检查的形式，让每一步都可被独立验证，从而把模型的自信转化为可审计的证据链。围绕定理证明助手与形式化数学库的一系列工作，正是沿着这一思路推进的。

另一个值得注意的维度是交互方式。数学研究很少是一次性给出完整答案的过程，更多时候是研究者与工具之间反复试探、逐步收敛的对话。如果AI系统被设计成只输出结论的黑箱，研究者就难以判断其推理路径是否可靠，也难以把模型的输出接续到自己的思路中去。相反，能够暴露中间步骤、允许质疑与追问、并如实表达不确定性的系统，才更贴近真实的研究工作流。

从更广的范围看，数学只是AI能力与人类专业需求之间可能发生错位的一个缩影。在法律、医疗、工程等同样强调严谨性的领域，类似的落差同样存在：模型擅长生成看似合理的文本，而专业人员真正需要的是可以被检验、可以被追责、可以被整合进既有流程的输出。把这种错位明确提出来，本身就是推动技术走向实用的一步。

对于关注AI技术演进的开发者来说，这篇文章的价值或许不在于给出某个具体结论，而在于提示了一个常被忽略的评估角度：衡量一个模型的能力，不应只看它在基准测试上的分数，还要看它与目标用户实际工作节奏之间的贴合程度。缩小这种错位，既需要模型能力的提升，也需要产品形态、验证机制与人机交互方式的共同调整。