15000ページの証明に、間違いが見つかった【有限単純群の分類定理】

有限単純群の分類定理の、15000ページの証明。その中に、1＝2になってしまう間違いが20年以上残っていました。この定理が何を言っているのか、間違いがどう見つかったのかを、正六角形とサッカーボールの群で見ていきます。 【目次】 0:00 イントロ 1:14 分類定理は、群について何を言い切っているのか 11:17 証明のどこが間違っていたのか 16:37 形式化とは何か、何十年も見つからなかった間違いはどう見つかったのか 24:09 人間とAIによる形式化は、何の役に立つのか 29:24 まとめ 【動画内で紹介した関連動画】 AI数学は正しいか？Lean（形式証明）の仕組みと限界    • AI数学は正しいか？Lean（形式証明）の仕組みと限界   【参考文献・資料】 [1] Axiom: Formalizing the Enormous Theorem https://axiommath.ai/research/the-eno... [2] Axiom: CFSG in Lean（証明の地図、参考文献、正誤の一覧） https://cfsg.axiommath.ai/ [3] Axiom: CFSG: selected departures from published arguments https://cfsg.axiommath.ai/CFSG_errata... [4] AxiomMath/CFSG（Leanのコード） https://github.com/AxiomMath/CFSG [5] M. Aschbacher, S. D. Smith: The Classification of Quasithin Groups I, II（American Mathematical Society、2004年） https://bookstore.ams.org/SURV/111 https://bookstore.ams.org/SURV/112 [6] 同じ本の、S. D. Smith さんが公開している原稿（1＝2の補題は付録EのE.2.2） http://homepages.math.uic.edu/~smiths... [7] M. Aschbacher: Highly complex proofs and implications of such proofs（Phil. Trans. R. Soc. A、2005年） https://authors.library.caltech.edu/r... [8] W. Feit, J. G. Thompson: Solvability of groups of odd order（Pacific Journal of Mathematics、1963年） https://msp.org/pjm/1963/13-3/pjm-v13... [9] 奇数位数定理のCoqでの形式化（math-comp/odd-order） https://github.com/math-comp/odd-order [10] L. Babai: Graph Isomorphism in Quasipolynomial Time https://arxiv.org/abs/1512.03547 [11] T. C. Burness: Simple groups, generation and probabilistic methods https://arxiv.org/abs/1710.10434 [12] Mathlib https://github.com/leanprover-communi... [13] Anthropic: Formalizing Fermat's Last Theorem https://www.anthropic.com/research/fo... [14] Scaling Verification of Cryptographic Software with Aeneas, Rust, and Lean https://arxiv.org/abs/2609.15648 [15] Madrona: Axiom についての記事 https://www.madrona.com/axiom-math-ca... 画像：Daniel Gorenstein　Konrad Jacobs / CC BY-SA 2.0 de https://commons.wikimedia.org/wiki/Fi... 画像：Michael Aschbacher　Katrin Schmid / CC BY-SA 2.0 de https://commons.wikimedia.org/wiki/Fi... 画像：Telstar（1970年のサッカーボール）　Zac allan / Public domain https://commons.wikimedia.org/wiki/Fi... 画像：元素の周期表　Offnfopt / Public domain https://commons.wikimedia.org/wiki/Fi... 画像：メンデレーエフの周期表（1869年）　Public domain https://commons.wikimedia.org/wiki/Fi... 画像：Camille Jordan　Public domain https://commons.wikimedia.org/wiki/Fi... 画像：Otto Hölder　Public domain https://commons.wikimedia.org/wiki/Fi... 画像：ボイジャー1号が撮った木星と土星　NASA https://commons.wikimedia.org/wiki/Fi... https://commons.wikimedia.org/wiki/Fi... 音声：VOICEVOX:ずんだもん 効果音：OtoLogic この動画は、原稿と図の作成の補助にAI（Claude）を使用しています。ただし内容の責任は、木村すらいむにあります。 【Twitter】   / kimu3_slime