用Lean 4和Claude形式化一个环论定理
作者分享了他使用Claude生成Lean 4代码以证明数学定理的实验。在成功验证了一些计算并经历了用Claude形式化半范数pqr定理的失败尝试后，这次他要求Claude正式证明一个环论定理。文章探讨了大语言模型在形式化验证中的能力与局限。
背景速读
John D. Cook是一位数学家和软件开发者，长期撰写数学、计算和编程方面的博客。Lean 4是一种交互式定理证明器（theorem prover），属于形式化验证（formal verification）工具——它用严格的形式逻辑检查数学证明的每一步是否正确，类似于让计算机“裁判”数学证明。Claude是Anthropic公司的大语言模型（LLM）。这篇文章记录了一个实验：让Claude直接生成Lean 4代码，来自动完成一道抽象代数定理的形式化证明。此前Cook曾成功让Claude验证一些具体计算，但让LLM写严格的形式化证明（特别是涉及“半范数的pqr定理”等抽象结构）难度大得多，那次尝试以失败告终。本文是后续尝试，测试当前LLM辅助形式化数学的能力边界，读者需要了解“定理证明器+大模型”这一交叉领域的发展现状。