350年の難問「フェルマーの最終定理」、コンピュータ証明に挑む数学者たち

フェルマーの最終定理をコンピュータ言語で新たに証明する

• インペリアル・カレッジ・ロンドンのケビン・バザード(Kevin Buzzard)教授が、2024年10月からフェルマーの最終定理(FLT)の形式証明をLean定理証明器で作成する予定です。
• 英国の工学・物理科学研究会議[EPSRC]が、バザード教授に同月から5年間、研究資金を支援することを決めました。
• Lean blueprintというplasTeXプラグインを用いて作成したプロジェクト計画書が、2024年4月末に公開される予定です。

フェルマーの最終定理はすでに証明されているのでは?

すでに証明されています。英国の数学者アンドリュー・ワイルズが1994年に証明を公開し、この証明は1995年に正式に出版されました。しかし、対話型定理証明器[ITP]の言語で書かれた形式証明はまだありません。

対話型定理証明器? 形式証明? それは何?

• 対話型定理証明器[ITP]: 人が形式証明を書くのを支援するコンピュータプログラム。証明支援系[proof assistant]とも呼ばれます。
• 形式証明: 証明検証器[proof verifier]というコンピュータプログラムで検証できる証明。証明支援系はたいてい証明検証器の役割も兼ねます。

定理証明器は人工知能なのか?

ニューラル定理証明器[NTP]はそう言えるかもしれませんが、Leanをはじめとする多くの対話型定理証明器は、機械学習ベースのプログラムではありません。

Lean定理証明器を紹介してほしい。

• 対話型定理証明器であると同時に、純粋関数型プログラミング言語でもあります。
• 依存型理論に基づいています。
• 型クラス、拡張可能な構文、マクロ、メタプログラミングなどの機能があります。
• 他の証明支援系と比べると、Leanの利用者層には(数学基礎論以外の分野を研究する)数学者がとりわけ多いです。

なぜフェルマーの最終定理の形式証明を書こうとしているのか?

ケビン・バザード教授がXに投稿したポストを引用すると、「コンピュータに現代整数論を理解させ、最終的には整数論研究者を支援できるようにするためです。」

リンク

• 2023年10月3日にケビン・バザード教授がLean Zulipチャットに投稿したメッセージ: https://leanprover.zulipchat.com/#narrow/stream/113486-announce/topic/…
• Leanの数学ライブラリ: https://github.com/leanprover-community/mathlib4
• New Scientistの記事: https://institutions.newscientist.com/article/…
• Popular Mechanicsの記事: https://popularmechanics.com/science/math/…

[calofmijuck]

応援しています。Formal proofに関心のある方は、Terrence Tao教授のMachine Assisted Proofs（https://youtube.com/watch/…