陶哲轩用GitHub Copilot和Lean的形式化工具，在完全不看高层逻辑、不理解证明结构的前提下，花33分钟“盲证”了一份人类写的一页纸证明。 证明的题目，是一道上世纪90年代就用计算机证明过，但从没人明确写出证明过程的题。 直到最近，这道题才由Bruno Le Floch大神给出了“1页纸”的人类手写版证明。 该题涉及一种代数结构“magma”，原命题“E1689”形式上是一个简单的等式，但实质上可以推出结构中所有元素相等，那叫一个复杂。 而陶哲轩的操作，可以说完全不动脑—— 他只管输入步骤，然后靠GitHub Copilot自动生成证明代码、Lean工具判对错，哪里报错就微调一下继续。 中途完全没有“大局观”，连命题是什么意思也不深究，就这么一行行跑下来，结果还真成了。 全程只花33分钟，比他手写花费的48分钟快了不少。 陶哲轩自己也说了，这种方法不适合有强结构/高概念的数学，但对于“符号堆砌”的证明，AI可能已经是最强工具人。 当然，AI也不是万无一失。实验中也有好几次Copilot给错了步骤、Lean卡壳、需要人手动修修补补。 但对比起完全靠人肉debug，效率已经天壤之别。 这场33分钟实验，背后透露出的，不只是AI对数学的“辅助”，更是下一代科研范式的雏形。 以后数学家也许不是坐在黑板前，而是坐在IDE前，和AI搭档、debug、互补完成证明任务，搞出新的结论。 原题目在这：-Equational/topic/Alternative.20proofs.20of.20E1689.E2.8A.A2E2 陶哲轩代码：
