这问题下展示了 AI 证明的常见错误用法，那就是直接问 AI，然后 AI 给出一堆伪证，你爱信不信吧。

问点稍微专业些的知识，一问三不知，瞎编第一名, 特别点名 DeepSeek。

不过特仑苏·陶的用法是正确的，那就是使用证明检查器，要求 AI 生成 Lean 代码。

陶在 AI 证明这个方向上还是非常清醒的。

全文可以看这篇 2024 年 12 月的访谈, 比较全面的展示了特仑苏·陶的观点。

Terence Tao AI Interview 我在此节选一部分对话以表明特…。