费马声称他关于费马大定理的证明太大，无法写在笔记本的页边距中。最近，在 Lean 代码中对费马大定理的形式化出现了一个漏洞。该漏洞是在利用 AI 进行代码审查实验时发现的。问题在于 Lean 的字符串切片函数在处理极大位置时的行为：逻辑上应返回空字符串，但编译后的代码却返回原始字符串。这种不一致导致了矛盾。定理证明器错误地得出空字符串等于非空字符串的结论，从而使得任何陈述（包括费马大定理）都能被证明。Lean 团队在漏洞报告后迅速修复了该问题。修复工作同时解决了内存安全和语义不匹配问题。尽管机器验证的证明提供了极高的可信度，但定理证明器本身的问题仍可能引发漏洞，因此对 Lean 证明进行仔细验证至关重要。