フェルマーは、ノートの余白には大きすぎる証明を彼の最終定理のために持っていたと主張しました。最近、Leanコードにおけるフェルマーの最終定理の形式化がバグを引き起こしました。このバグは、コードレビューのためのAIを実験中に発見されました。この問題は、Leanの文字列スライス機能が極端に大きな位置をどのように処理するかに影響します。論理的には空文字列を返すはずですが、コンパイルされたコードは元の文字列を返します。この不一致は矛盾を生み出します。定理証明器は、空文字列が非空文字列と等しいと誤って結論付けます。これにより、フェルマーの最終定理を含むあらゆる命題を証明することが可能になります。Leanチームは、報告後、驚くほど迅速にバグを修正しました。修正には、メモリ安全性と意味論的な不一致の両方に対処することが含まれていました。機械チェックされた証明は大きな信頼を提供しますが、定理証明器の問題から脆弱性が生じる可能性があります。したがって、Lean証明の慎重な検証が不可欠です。