Loading article…
コンピュータ支援証明とは、少なくとも部分的にコンピュータによって生成された数学的な証明です。
これまでのコンピュータ支援による証明のほとんどは、数学の定理の大規模な網羅的証明の実装でした。その考え方は、コンピュータ プログラムを使用して長い計算を実行し、これらの計算の結果が特定の定理を意味することを証明することです。1976 年、4 色定理はコンピュータ プログラムを使用して検証された最初の主要な定理でした。
人工知能研究の分野では、ヒューリスティック検索などの自動推論技術を使用して、数学の定理のより小さく明示的な新しい証明をボトムアップで作成する試みも行われてきました。このような自動定理証明器は、いくつかの新しい結果を証明し、既知の定理の新しい証明を見つけました。[要出典] さらに、対話型証明アシスタントにより、数学者は人間が読める証明を作成し、それにもかかわらず正しさを正式に検証することができます。これらの証明は一般に人間が調査可能であるため（ロビンズ予想の証明のように困難ではありますが）、コンピューター支援による網羅的証明の物議を醸す意味合いを共有しません。
方法
数学の証明にコンピュータを使用する方法の 1 つは、いわゆる検証済み数値または厳密な数値を使用する方法です。これは、数値的に計算しながらも数学的に厳密であることを意味します。数値プログラムの集合値出力が元の数学の問題の解を囲むようにするために、集合値演算と包含原理 [明確化]を使用します。これは、たとえば区間演算を使用して、丸め誤差と切り捨て誤差を制御、囲み、伝播することによって行われます。より正確には、計算を一連の基本操作、たとえば に簡略化します。コンピュータでは、各基本操作の結果はコンピュータの精度で丸められます。ただし、基本操作の結果の上限と下限によって提供される区間を構築できます。次に、数を区間に置き換え、表現可能な数のそのような区間間で基本操作を実行します。[引用が必要]
哲学的な反論
コンピュータ支援による証明は数学界で論争の的となっているが、トーマス・ティモツコが最初に異議を唱えた。ティモツコの主張を支持する人々は、コンピュータ支援による長い証明は、人間が検証できないほど多くの論理的ステップを含むため、ある意味では「本当の」数学的証明ではないと信じている。また、数学者は事実上、仮定された公理からの論理的演繹を、コンピュータ プログラムのエラーや実行環境およびハードウェアの欠陥の影響を受ける可能性のある経験的計算プロセスへの信頼に置き換えるよう求められていると考えている。 [1]
他の数学者は、コンピュータ支援による長い証明は証明ではなく計算とみなすべきだと考えている。証明アルゴリズム自体が有効であることが証明されなければ、その使用は単なる「検証」とみなされる。コンピュータ支援による証明はソース プログラム、コンパイラ、ハードウェアでエラーが発生する可能性があるという議論は、コンピュータ プログラムの正しさの正式な証明を提供すること ( 2005 年に4 色定理に適用されて成功したアプローチ) と、異なるプログラミング言語、異なるコンパイラ、異なるコンピュータ ハードウェアを使用して結果を再現することで解決できる。
コンピュータ支援による証明を検証する別の方法としては、推論手順を機械可読形式で生成し、証明チェッカープログラムを使用してその正しさを証明する方法があります。与えられた証明を検証するのは証明を見つけるよりもはるかに簡単なので、チェッカー プログラムは元のアシスタント プログラムよりも単純で、その正しさに対する信頼を得るのもそれに応じて簡単です。ただし、コンピュータ プログラムを使用して別のプログラムの出力が正しいことを証明するというこの方法は、コンピュータ証明懐疑論者には魅力的ではありません。彼らは、この方法は人間の理解の必要性に対処せずに複雑さをさらに増すだけだと考えています。
コンピュータ支援による証明に対するもう一つの反論は、コンピュータ支援による証明には数学的な優雅さが欠けている、つまり、コンピュータ支援による証明は洞察や新しい有用な概念を提供しないというものである。実際、これはどんな長い証明に対しても徹底して反論できる反論である。
コンピュータ支援による証明によって生じるもう 1 つの哲学的問題は、コンピュータ支援による証明によって数学が準経験科学になるかどうか、つまり抽象的な数学概念の領域において科学的方法が純粋理性の適用よりも重要になるかどうかです。これは、数学が観念に基づいているのか、それとも「単なる」形式的な記号操作の練習にすぎないのかという数学内の議論に直接関係しています。また、プラトン主義の見解によれば、すべての可能な数学的対象が何らかの意味で「すでに存在している」のであれば、コンピュータ支援による数学は物理学や化学のような実験科学ではなく、天文学のような観測科学であるかどうかという疑問も生じます。数学内のこの論争は、21 世紀の理論物理学が数学的になりすぎて、実験的ルーツを捨て去っているのではないかという疑問が物理学界で提起されているのと同時に起こっています。
実験数学という新興分野では、数学的探究の主なツールとして数値実験に焦点を当てることで、この議論に正面から取り組んでいます。
コンピュータプログラムの助けを借りて証明された定理
このリストに含まれていることは、正式なコンピュータチェック済みの証明が存在することを意味するのではなく、コンピュータ プログラムが何らかの形で関与していることを意味します。詳細については、メインの記事を参照してください。
- 共通不動点問題、1967年[2]
- 四色定理、1976年[3]
- ミッチェル・ファイゲンバウムの非線形力学における普遍性予想。1982年にOEランフォードが厳密なコンピュータ演算を使用して証明した。
- コネクトフォー、1988年 – 解決されたゲーム
- 10次の有限射影平面の非存在、1989年
- ダブルバブル予想、1995年[4]
- ロビンズ予想、1996年
- ケプラー予想、1998年 – 箱の中に球を最適に詰める問題
- ローレンツアトラクター、2002年 -スメールの問題の14番目は、区間演算を使用してワーウィック・タッカーによって証明されました。
- ハッピーエンド問題の17点事例、2006年
- Kouril [5] [6] [7]（2006年から2016年の間）は、 FPGAベースのSATソルバーを使用していくつかのファンデルワールデン数を計算しました。
- 最小重量三角形分割のNP困難性、2008年
- Ahmed [8] [9] [10] [11] [12]は（2009年から2014年の間に）DPLLアルゴリズムベースのスタンドアロンおよび分散SATソルバーを使用していくつかのファンデルワールデン数を計算しました。Ahmedは2010年に初めてクラスター分散SATソルバーを使用してw(2; 3, 17) = 279とw(2; 3, 18) = 312を証明しました。[9]
- ルービックキューブの最適解は最大20面移動で得られる、2010年[13]
- 解ける数独パズルの最小ヒント数は17です。2012年
- 2014年にエルデシュの矛盾問題の特殊なケースがSATソルバーを使って解かれた。その後、完全な予想はコンピュータの助けを借りずにテレンス・タオによって解かれた。[14]
- 2016年5月に200テラバイトのデータを使用してブールピタゴラスの三つ組の問題が解決されました。[15]
- コルモゴロフ-アーノルド-モーザー理論への応用[16] [17]
- ランクが5以上の自由群の自己同型群に対するカジダンの性質（T）
- シューア数5、S(5) = 161の証明は2017年にマライン・ホイレによって発表され、2ペタバイトのスペースを占めた[18] [19]
- 7次元のケラー予想は2020年現在、200ギガバイトの証明を持つ唯一のケースである[20] [21]
- 無限正方格子のパッキング彩色数は15であり、2023年にスベルカソーとヒュールによって発表された[22] [23] （平面の彩色数に関するハドヴィガー・ネルソン問題も参照）
参照
- 形式検証 – 特定のアルゴリズムの正しさを証明または反証すること
- Logic Theorist – 1956年にアレン・ニューウェル、ハーバート・A・サイモン、クリフ・ショーによって書かれたコンピュータプログラム
- 数学的証明 – 数学的記述の推論
- Metamath – 形式言語と関連するコンピュータプログラム
- モデル検査 – コンピュータサイエンス分野
- Seventeen or Bust – 素数を研究する BOINC ベースのボランティア コンピューティング プロジェクト
- 記号計算 – コンピュータサイエンスと数学の境界にある科学分野
- 検証済み数値 – 数学的に厳密なエラー評価を含む数値
参考文献
- ^ Tymoczko, Thomas (1979)、「4色問題とその数学的意義」、The Journal of Philosophy、76 (2): 57–83、doi :10.2307/2025976、JSTOR 2025976。
- ^ Boyce, William M. (1969 年 3 月). 「共通の固定点を持たない可換関数」(PDF) .アメリカ数学会誌. 137 : 77–92. doi :10.1090/S0002-9947-1969-0236331-5.
- ^ Gonthier, Georges (2008)、「形式的証明 - 4色定理」(PDF)、アメリカ数学会誌、55 (11): 1382–1393、MR 2463991、2011-08-05のオリジナルからアーカイブ(PDF)
- ^ Hass, J.; Hutchings, M.; Schlafly, R. (1995). 「二重バブル予想」.アメリカ数学会電子研究発表. 1 (3): 98–102. CiteSeerX 10.1.1.527.8616 . doi :10.1090/S1079-6762-95-03001-0.
- ^ Kouril, Michal (2006)。マルチクラスター計算と Sat ベンチマーク問題の実装への拡張を備えた Beowulf クラスターのバックトラッキング フレームワーク (博士論文)。シンシナティ大学。
- ^ コウリル、ミハル (2012). 「ファンデルワールデン数W(3,4)=293の計算」。整数。12：A46。MR 3083419。
- ^ Kouril, Michal (2015)。「SAT 計算のための FPGA クラスターの活用」。並列コンピューティング: エクサスケールへの道: 525–532。
- ^ タンビール、アーメド (2009)。 「いくつかの新しいファンデルワールデン番号といくつかのファンデルワールデンタイプの番号」。整数。9：A6．土井：10.1515/integ.2009.007。MR 2506138。S2CID 122129059 。
- ^ ab Ahmed, Tanbir (2010). 「2つの新しいファンデルワールデン数 w(2;3,17) と w(2;3,18)」.整数. 10 (4): 369–377. doi :10.1515/integ.2010.032. MR 2684128. S2CID 124272560.
- ^ タンビール、アーメド (2012)。 「正確なファンデルワールデン数の計算について」。整数。12 (3): 417–425。土井：10.1515/integ.2011.112。MR 2955523。S2CID 11811448 。
- ^ Ahmed, Tanbir (2013). 「その他の Van der Waerden 数」. Journal of Integer Sequences . 16 (4): 13.4.4. MR 3056628.
- ^ Ahmed, Tanbir; Kullmann, Oliver; Snevily, Hunter (2014). 「ファンデルワールデン数 w(2;3,t) について」.離散応用数学. 174 (2014): 27–51. arXiv : 1102.5433 . doi : 10.1016/j.dam.2014.05.007 . MR 3215454.
- ^ 「神の数字は20」cube20.org 2010年7月。 2023年10月18日閲覧。
- ^ Cesare, Chris (2015年10月1日). 「数学の達人が名人の謎を解く」. Nature . 526 (7571): 19–20. Bibcode :2015Natur.526...19C. doi : 10.1038/nature.2015.18441 . PMID 26432222.
- ^ Lamb, Evelyn (2016年5月26日). 「200テラバイトの数学証明は史上最大」. Nature . 534 (7605): 17–18. Bibcode :2016Natur.534...17L. doi : 10.1038/nature.2016.19990 . PMID 27251254.
- ^ Celletti, A.; Chierchia, L. (1987). 「コンピュータ支援KAM理論の厳密な推定」. Journal of Mathematical Physics . 28 (9): 2078–86. Bibcode :1987JMP....28.2078C. doi :10.1063/1.527418.
- ^ Figueras, JL; Haro, A.; Luque, A. (2017). 「KAM理論の厳密なコンピュータ支援アプリケーション：最新のアプローチ」.計算数学の基礎. 17 (5): 1123–93. arXiv : 1601.00084 . doi :10.1007/s10208-016-9339-3. hdl :2445/192693. S2CID 28258285.
- ^ Heule、Marijn JH (2017). 「シュール第五番」。arXiv : 1711.08076 [cs.LO]。
- ^ 「Schur Number Five」www.cs.utexas.edu . 2021年10月6日閲覧。
- ^ ジョシュア・ブラケンジーク;ヘーレ、マリジン。マッキー、ジョン。ナルバエス、デイビッド (2020)。 「ケラー予想の解決」。ペルチェでは、ニコラ。ソフロニー＝ストッカーマンズ、ヴィオリカ（編）。自動推論。コンピューターサイエンスの講義ノート。 Vol. 12166.スプリンガー。 48–65ページ。土井：10.1007/978-3-030-51074-9_4。ISBN 978-3-030-51074-9. PMC 7324133 .
- ^ Hartnett, Kevin (2020-08-19). 「コンピューター検索が90年前の数学の問題を解決」. Quanta Magazine . 2021-10-08閲覧。
- ^ Subercaseaux, Bernardo; Heule, Marijn JH (2023-01-23). 「無限正方格子のパッキング彩色数は15です」. arXiv : 2301.09757 [cs.DM].
- ^ Hartnett, Kevin (2023-04-20). 「数字15は無限グリッドの秘密の限界を表す」. Quanta Magazine . 2023-04-20閲覧。
さらに読む
- Lenat, DB (1976)。AM: 数学における発見への人工知能アプローチ、ヒューリスティック検索(PDF) (PhD)。AI ラボ、スタンフォード大学。STAN-CS-76-570、ヒューリスティック プログラミング プロジェクト レポート HPP-76-8。
- Meyer, KR; Schmidt, DS 編 (2012)。解析におけるコンピュータ支援証明。IMA 数学とその応用巻。第 28 巻。Springer。ISBN 978-1-4613-9092-3。
- 中尾 正之; プラム 正之; 渡辺 勇治 (2019)。偏微分方程式の数値検証法とコンピュータ支援証明。Springer 計算数学シリーズ。Springer。ISBN 9789811376696。
外部リンク
- Lanford, Oscar E. (1982). 「ファイゲンバウム予想のコンピュータ支援による証明」(PDF) . Bull. Amer. Math. Soc . 6 (3): 427–434. CiteSeerX 10.1.1.434.8389 . doi :10.1090/S0273-0979-1982-15008-X.
- Furse, Edmund (1990)。なぜ AM は勢いを失ったのか? (技術レポート)。グラモーガン大学コンピューター研究科。CS-90-4。2012 年 7 月 17 日時点のオリジナルよりアーカイブ。2016年 9 月 6 日閲覧。
{{cite tech report}}: CS1 maint: bot: 元の URL ステータス不明 (リンク) - Begley, S. (2018 年 4 月 16 日)。「コンピューターによる数値証明は誤りを起こす可能性がある」。Pittsburgh Post-Gazette。2018年 4 月 16 日時点のオリジナルよりアーカイブ。
- 「形式的証明に関する特別号」。アメリカ数学会の通知。2008 年 12 月。