【形式証明付き】余白に収まるフェルマーの最終定理の証明【AI不使用】

/- Fermat's Last character is T! -/
theorem FLT : "Fermat".toList.getLast! = 't' := rfl

これは何？

フェルマーの最終定理、つまり「Fermat(フェルマー)の最終文字はt」の証明です。証明の各ステップは定理証明支援系Leanによって正しさが検証されています。

この記事は何？

形式的証明があるということは、数学的主張が正しいことを意味しません。何が形式化され、何が証明されたのかを注意深く確認する必要があります。

Leanをはじめとする定理証明支援系を使う際には、数学的主張を定理証明支援系の文法に翻訳（形式化）する必要があります。しかし、定理証明支援系がチェックしてくれるのは「形式化された主張」と「形式化された証明」が噛み合っているかどうかまでで、それが人々が元々意図していた数学的主張と一致しているかどうかまでは保証してくれません。

つまり、誰かが「○○の定理を（Lean/Rocq/Isabelleで）証明した」と言っても、それが本当に人間の意図した通りの定理・証明かどうかは、個別に確認する必要があるのです。

特に、大規模言語モデル（LLM）を使って形式的証明を生成した場合には注意が必要です。「○○を証明せよ」というプロンプトに忠実になろうとするあまり、定義や定理文が（気づかないうちに）想定外の方向に捻じ曲がってしまうおそれがあるからです^[1]。

もし、重大な未解決問題の形式的証明を見かけたとしても、拡散する前にまずは落ち着きましょう。その中身が「Fermatの最終文字はt」みたいに、意味の無い別物の主張になっている可能性もあります。定義や証明方針について、専門家による確認を待つのが安全です。

それでも証明したい！

それでもあなたが未解決問題に取り組むとしたら、以下のような方法を試してみてください。

• 教科書や既存の論文を読み、対象分野の理解を深めましょう。
• 形式化された定義や主張が、その分野で一般に受け入れられている定義や定式化と一致しているか確認しましょう。
• DeepMindが未解決問題（予想）に関する定義を多数形式化して公開しています：https://github.com/google-deepmind/formal-conjectures
  • ただし、このリポジトリでも形式化ミスがしばしば見つかっています：https://github.com/google-deepmind/formal-conjectures/issues?q=label%3Amisformalization

形式化は難しいのです。そしてその難しさが定理証明支援系のおもしろみでもあります。あなたの定理証明に幸あらんことを。

脚注

1. さらに手前の問題として、プロジェクトのセットアップがおかしかったり、不適切な公理を導入していたりして何でも証明できる状態になっていることもあります。