長文の数学的証明一覧

これは、非常に長い数学的証明 のリストです。このような証明は、計算による証明手法を用いることが多く、概観することが困難であると考えられます。

2011年現在掲載された論文ページ数で測った最長の数学的証明は、有限単純群の分類に関するもので、1万ページをはるかに超える。もしそれらが依拠するコンピュータ計算の詳細がすべて公開されれば、これよりもはるかに長くなるであろう証明がいくつか存在する。

異常に長い証明の長さは、時代とともに増加している。大まかな目安として、1900年で100ページ、1950年で200ページ、2000年で500ページは、証明としては異常に長いと言える。

• 1799年 –アーベル＝ルフィーニの定理はパオロ・ルフィーニによってほぼ証明されたが、500ページに及ぶ彼の証明はほとんど無視され、その後1824年にニールス・ヘンリック・アーベルがわずか6ページで証明を発表した。
• 1890年 –キリングによる単純複素リー代数の分類（例外リー代数の発見を含む）は、4つの論文で180ページにわたって行われた。
• 1894年 –ヨハン・グスタフ・ヘルメスによる、定規とコンパスを用いた65537辺の多角形の作図は、200ページ以上に及んだ。
• 1905年 –エマニュエル・ラスカーによるラスカー＝ネーターの定理の最初の証明は98ページに及んだが、その後簡略化され、現代の証明は1ページ未満となっている。
• 1963年 –フェイトとトンプソンによる奇数位数の定理は255ページにも及び、当時群論における長文論文と考えられていたものの10倍以上の長さだった。
• 1964年 –特異点の解消。広中氏の元の証明は216ページにも及んだが、その後大幅に簡略化され、現在では10～20ページ程度になっている。
• 1966年、アビヤンカーは標数が6より大きい3次元多様体における特異点解消の証明を複数の論文で発表し、その論文は約500ページに及んだ。2009年、カットコフスキーはこの証明を約40ページに簡略化した。
• 1966年 –リー群の離散級数表現。ハリシュ・チャンドラによるこれらの表現の構築には、合計約500ページに及ぶ一連の論文が必要だった。その後、半単純群に対するプランシュレル定理に関する研究で、さらに150ページが追加された。
• 1968年 –ノビコフとアディアンの証明により、有限生成無限群における有限指数に関するバーンサイドの問題が否定的に解決された。この3部構成の原論文は300ページ以上に及ぶ。（後にブリットンが282ページの論文を発表し、この問題の解決を試みたが、彼の論文には重大な欠陥があった。）
• 1960～1970年 – 『代数幾何学の基礎』、 『代数幾何学の素質』、そして『代数幾何学セミナー』 。グロタンディークの代数幾何学の基礎に関する著作は、数千ページに及ぶ。本書は単一の定理の証明ではないものの、その証明が数百ページに及ぶ先行研究に基づいている定理が複数含まれている。
• 1974年 – N群定理。トンプソンのN群の分類は、合計約400ページに及ぶ6つの論文に基づいているが、奇数位数定理などの以前の結果も使用しており、合計で700ページを超える長さになっている。
• 1974年 –ラマヌジャン予想とワイル予想。これらの予想を証明するデリーニュの最終論文は「わずか」30ページ程度だったが、その背景にある代数幾何学とエタールコホモロジーの結果は、デリーニュ自身が約2000ページと見積もったものであった。
• 1974年 – 4色定理。アペルとハーケンによるこの定理の証明は139ページに及び、長時間のコンピュータ計算にも依存していた。
• 1974年 –ゴレンシュタイン・ハラダの定理は、区分的2階数が最大4の有限群を分類するもので、464ページにも及ぶ。
• 1976年 –アイゼンシュタイン級数。ラングランズによるアイゼンシュタイン級数の関数方程式の証明は337ページに及ぶ。
• 1983年 –三分割定理。ゴレンシュタインとライオンズによるランクが4以上の場合の証明は731ページに及び、アシュバッハーによるランク3の場合の証明はさらに159ページ加わり、合計890ページとなった。
• 1983年 –セルバーグトレース公式。ヘイハルによるセルバーグトレース公式の一般形の証明は、合計1322ページ、2巻から成っていた。
• アーサー・セルバーグのトレース公式。アーサーによるこの公式の様々なバージョンの証明は、多くの論文にわたって数百ページに及ぶ。
• 2000年 –アルムグレンの正則性定理。アルムグレンの証明は955ページに及ぶ。
• 2000年 –関数体上の一般線形群に関するラングランズ予想についてのラフォルグの定理。ローラン・ラフォルグによるこの定理の証明は、背景となる結果に関する多くのページを除いても、約600ページに及ぶ。
• 2003年 –ポアンカレ予想、幾何化定理、幾何化予想。ペレルマンによるポアンカレ予想と幾何化予想の元の証明は長文ではなく、むしろ概略的なものであった。他の数人の数学者が詳細を補足した証明を発表しており、それらは数百ページに及ぶ。
• 2004年 –クアシシン群。アシュバッハーとスミスによる単純クアシシン群の分類は1221ページに及び、これまでに書かれた単一論文の中で最も長いものの1つである。
• 2004年 –有限単純群の分類。この証明は数百もの学術論文に分散しているため、その総ページ数を正確に見積もることは困難だが、おそらく1万ページから2万ページ程度だろう。
• 2004年 –ロバートソン・シーモアの定理。証明は約20本の論文にまたがり、約500ページに及ぶ。
• 2005年 –ケプラー予想。ヘイルズによるこの予想の証明は、数百ページに及ぶ論文と、数ギガバイトに及ぶコンピュータ計算に基づいている。
• 2006年 –マリア・チュドノフスキー、ニール・ロバートソン、ポール・シーモア、ロビン・トーマスによる「強力な完全グラフ定理」 。この論文は『Annals of Mathematics』誌に180ページにわたって掲載された。

長時間のコンピュータ計算によって検証された数学定理は数多く存在します。これらを証明として書き出すと、多くは上記の証明のほとんどよりもはるかに長くなります。コンピュータ計算と証明の間には明確な区別はありません。上記の証明のいくつか、例えば4色定理やケプラー予想などは、長時間のコンピュータ計算と何ページにも及ぶ数学的議論の両方を用いています。このセクションのコンピュータ計算では、数学的議論はわずか数ページであり、その長さは長時間ではあるものの定型的な計算によるものです。このような定理の典型的な例としては、以下のようなものがあります。

• ライオンズ群のような散在単純群の存在証明は、当初、大規模な行列や数十億個の記号の順列を用いたコンピュータ計算によって行われていました。ベビーモンスター群のようなほとんどの場合、コンピュータによる証明は後に、コンピュータ計算を回避したより簡潔な証明に置き換えられました。同様に、より大きな散在群の最大部分群の計算には、多くのコンピュータ計算が用いられています。
• 特定の数が素数であることを証明する
• 2004年 –リーマンゼータ関数の最初の10 ^13個の零点に対するリーマン予想の検証。
• 2007年 –チェッカーが引き分けであることを検証。
• πの多数の桁の計算。
• 2010年 –ルービックキューブを20手で解けることを証明。
• 2012年 – 数独には少なくとも17個のヒントが必要であることを示す。
• 2013年 –三項ゴールドバッハ予想：5より大きいすべての奇数は、3つの素数の和として表すことができる。
• 2014年 –エルデシュの不一致予想の特定のケースC =2に対する証明：長さ1161のすべての±1シーケンスは少なくとも3の不一致を持つ。SATソルバーによって生成された元の証明は13ギガバイトのサイズであったが、後に850メガバイトに縮小された。
• 2016年 –ブールピタゴラス三つ組問題の解決には、200テラバイトの証明の生成が必要だった。^{[ 1 ]}
• 2017年 –ブールピタゴラス三つ組問題の解法を共同執筆したマリイン・ホイレは、5番目のシュール数が160であることを示す2ペタバイトの長さの証明を発表した。^{[ 2 ]}

クルト・ゲーデルは、形式体系において証明可能であるにもかかわらず、最短の証明が途方もなく長くなる命題の具体的な例を見つける方法を示した。例えば、次の命題である。

「この命題は、グーゴルプレックス記号未満のペアノ算術では証明できない」

ペアノ算術では証明可能ですが、最短の証明でも少なくともグーゴルプレックス個の記号が必要です。より強力な体系では短い証明が可能です。実際、ペアノ算術では、ペアノ算術が無矛盾であるという命題（これはゲーデルの不完全性定理ではペアノ算術では証明できません）とともに容易に証明できます。

この議論では、ペアノ算術はより強力で一貫性のあるシステムに置き換えることができ、グーゴルプレックスは、そのシステムで簡潔に記述できる任意の数に置き換えることができる。

ハーヴェイ・フリードマンはこの現象の明確な自然例をいくつか発見し、ペアノ算術やその他の形式体系において、最短証明が途方もなく長い明示的な命題をいくつか挙げた（スモリンスキー 1982 ）。例えば、命題

「ある整数nが存在し、根付き木の列T ₁ , T ₂ , ..., T _nが存在し、 T _{k の}頂点数が最大でk + 10 であるならば、ある木は後の木に同相的に埋め込むことができる。」

ペアノ算術では証明可能ですが、最短の証明の長さは少なくとも¹⁰⁰⁰ 2 であり、⁰ 2 = 1 および^{n +1} 2 = 2 ^{( n 2)} (四項成長) です。この命題はクラスカルの定理の特殊な場合であり、 2 階算術では短い証明があります。

• 不完全な証明のリスト
• 脅迫による証明

• Krantz, Steven G. (2011), 『証明はプディングの中にある。数学的証明の変容する性質』（PDF）、ベルリン、ニューヨーク：Springer-Verlag、doi：10.1007/978-0-387-48744-1、ISBN 978-0-387-48908-7MR 2789493​ 
• Smoryński, C. (1982), "樹木経験の多様性", Math. Intelligencer , 4 (4): 182–189 , doi : 10.1007/bf03023553 , MR 0685558 , S2CID 125748405