数学者もブラックな冗談を言う

【 数学者もブラックな冗談を言う 】

2012年、Georges Gonthierは、Coqを用いて、群論のFeit–Thompson 定理の形式的証明に成功しました。

この定理は、1962-1963年にWalter Feit と John Griggs Thompson によって証明された、群論の基本的な定理の一つです。この定理は、「奇数位数の有限単純群は可解である」ことを主張し(「奇数位数定理 = “Odd Order Theorem” とも呼ばれます )、有限単純群の分類問題で重要な役割を果たしています。

「有限単純群の分類問題」は、Daniel Gorensteinをリーダーとする数学者の集団によって解決され、20世紀の数学の大きな成果の一つと呼ばれています。

ただ、その「証明」は、100人以上の数学者が、50年のあいだに数百の論文誌に発表した、膨大な量の「証明」の総和です。そのページ数は一万ページを超えると言われています。

証明が、あまりに膨大なので、

 「この証明を全部を読んでる数学者は、1人もいない。」

というブラック・ジョークがあるそうです。

でも、数学の証明を行うのに、過去の数学の論文を全部読む必要は、実はないのです。それについては、また別の機会に説明したいと思います。

【 「Feit–Thompson定理の形式的証明」を公開しました。 】

スライドのpdfは、こちらからアクセスできます。
https://drive.google.com/file/d/1zN_-J2KbwuKs_DEeapY_0P5-rtidnH4B/view?usp=sharing

このトピックのまとめページは、こちらです。ほぼ毎日更新されると思います。https://www.marulabo.net/docs/math-proof/

セミナーへのお申し込みは、こちらからお願いします。
https://math-proof.peatix.com/

コメント

このブログの人気の投稿

マルレク・ネット「エントロピーと情報理論」公開しました。

初めにことばありき

人間は、善と悪との重ね合わせというモデルの失敗について