它生成了与之前形式化证明结构相似的代码，并成功定义了关键的幂函数。

然而，陶哲轩创建一个新文件，在Claude编译过程中，却发现错误——它假设从自然数1开始，而Lean中的自然数从0开始。

另外，Claude未能正确处理方程的对称性，比如x=(y·x)·z，导致了证明逻辑出现偏差。

尽管单行代码生成高效，但缺乏对整体结构的理解，使得错误诊断和修复变得困难。

通过人工干预，陶哲轩修复了这些问题，最终在20分钟内完成形式化。