当AI给出20万行不可读的证明，数学还是数学吗？

AI公司Math Inc利用Gauss模型，自主完成了菲尔兹奖级别难题的Lean语言形式化证明。但这在数学界引发了巨大争议：这串长达20万行的代码虽然通过了机器验证，但在人类眼中却是一坨不可审计、无法维护的逻辑乱码。

这件事揭示了数学认知的底层冲突：证明的目的是为了获得一个“正确”的结论，还是为了建立可复用的认知抽象？

人类数学史是一部“API进化史”。我们将复杂的推导封装成优雅的定理和引理，让后人不必重造轮子。而AI目前的证明方式更像是在暴力搜索逻辑空间，它产出的是“二进制结果”而非“源代码”。这种不可读的证明虽然拿到了结果，却无法提供能启发下一场科学革命的洞见。

如果数学研究演变为向AI“求签”，人类将从真理的发现者退化为神谕的维护者。真正的挑战不在于AI能否解决难题，而在于当真理的尺度超越了人类直觉的极限，我们是否愿意接受一个只有结果、没有过程的“黑盒文明”。

spectrum.ieee.org/ai-in-mathematics

#人工智能##AI创造营##数学##形式化验证##Token#