陶哲轩大家都很熟了，被誉为“数学界的莫扎特”的超级大神
今天，陶神在社交媒体 Mastodon (@tao@mathstodon.xyz) 上分享了一次AI协作实验：他尝试使用当前流行的AI自动化工具，来形式化（formalize）一个数学证明。具体来说，他用的是 GitHub Copilot 配合 Lean (一个依赖类型理论的证明助手) 中的 canonical 策略 (一个依赖类型匹配策略)
目标：搞定一个“小”证明，但需要极高精确度的“体力活”证明
这次实验的对象，是陶哲轩在“等式理论项目 (Equational Theories Project)”中的一位合作者 Bruno Le Floch 提供的一页纸证明。这个证明属于泛代数领域，具体来说，是关于“原群 (magma)”（一个集合配上一个二元运算，不一定满足结合律啥的）的一些定律
核心是要证明一个编号为 e1689 的等式
能推导出 e2 等式（x = y 对任意 x, y 成立，即所谓的“单点律”）。这个推导过程充满了繁琐的符号操作，不涉及太多高深概念，主要考验细节的准确性
大神“盲打”：33分钟的AI辅助之旅
陶哲轩的目标是，以一种“低级别”、“逐行”的方式，几乎是“盲打”地，在不深入理解证明宏观结构的前提下，完成这个形式化过程。他想看看AI工具能在多大程度上助力这种技术性工作
你可能以为大神一出手就马到成功？非也！陶神坦言，这是他的第三次尝试：
-
• 第一次：没看证明，直接上手写代码，结果5行就卡住了，因为不理解其中一步 -
• 第二次：完整地走完了流程，耗时48分钟，但悲催的是屏幕录制出了问题 -
• 第三次（也就是这次分享的）：因为已经做过一次，所以“心中有数”，仅用33分钟就完成了。他也幽默地提到，AI工具可能因为他之前的尝试而被“污染”了，或许已经“记住”了部分证明。所以，这算不上一个严格的科学对照实验，但足以展示过程
实验过程亮点（浓缩版）：
1.环境搭建：首先在 Lean 中定义了“原群 (Magma)”、e1689 和 e2 等基本概念
2.逐行翻译：陶哲轩将 Bruno 的证明拆分成一个个“原子级”的小步骤，然后逐行尝试形式化
-
• 定义辅助对象：比如定义了函数 S(x, z) = x * x * z * z和F(x, y, z) = y * S(x, z)（后来发现F其实是y * (x * (x * z * z))）。主等式 e1689 可以写成x = F(x, y, z) -
• Copilot 的角色：GitHub Copilot 会在他输入时提供代码建议。有时建议很精准，能直接采用；有时则需要手动调整，甚至会给出错误的中间结论，需要陶哲轩识别并修正。比如在证明 Lemma 1 的一个计算步骤中，Copilot 给出的 FBC = A * B * Z就和实际需要的A * F B C（或A * Z，其中Z是SCB）不符 -
• canonical策略的运用：canonical策略在很多类型匹配上表现出色，能自动完成一些简单的证明步骤。但陶哲轩也提到，在处理存在性量词（比如证明“存在一个 z 使得 y = z * a”）时，canonical有时会“卡住”，需要他手动“打开”这个存在性量词（即明确指出这个 z 是什么），canonical才能继续工作 -
• “卡壳”与手动介入：当AI工具无法一步到位时，陶哲轩会查阅 Bruno 的原始证明，理解当前步骤的逻辑，然后使用 Lean 中更基础的策略（如 apply,exact,convert,calc计算块等）进行手动推导，直到问题简化到AI工具可以接手的程度 -
• Lemma 的逐个击破：整个证明被分解为多个 Lemma (引理)
3.最终定理证明：基于前面的引理，最后证明了 e1689 能够推导出 e2 (a = y)。其中一个关键步骤是，利用 Lemma 3 得到的 e，将 a 表示为 S(e,a)，然后代入主等式进行推导
注意：以上过程只是简单示意总结，难免出错，数学大神请直接看陶神视频
这是最终证明：
https://github.com/teorth/estimate_tools/blob/master/EstimateTools/test/equational.lean
陶哲轩的思考：AI辅助下的新范式
实验结束后，陶哲轩总结道：
风格迥异：这种高度依赖AI工具、逐行解决细节的方式，与他平时先理解证明“大局观”再进行形式化的风格完全不同
效率与盲点：对于这种技术性强、概念性不那么突出、主要考验细节准确性的证明（陶神称之为“非概念性论证”），AI工具组合确实能有效工作。它把主要精力从“理解宏观策略”转移到了“确保每一步细节正确”
人机协作是关键：AI工具并非万能。大约一半时间，工具能直接给出正确步骤；另一半时间，则需要人工阅读原始证明，甚至动用“老派”的证明技巧来化简问题，然后再让AI接手。期间，他也因过度依赖Copilot而错过检查其生成的语句是否确实是证明所需要的，导致返工
“剥离概念，聚焦细节”：整个过程几乎没有进行高层次的策略思考，而是将证明分解为一系列“完成下一行代码”的小问题
适用场景：这种方法可能非常适合处理那些本身就比较繁琐、缺乏巧妙思想但又需要极高精确度的“体力活”证明
参考：
https://www.youtube.com/watch?v=cyyR7j2ChCI&t=9s
⭐
（文：AI寒武纪）