計算機援用証明

計算機援用証明とは、コンピュータによって少なくとも一部が生成された数学的証明である^[1]。今日における計算機援用証明のほとんどは数学的定理に対するしらみつぶし法（英語版）の実装である。具体的には、膨大で複雑な計算をコンピュータによって実行し、計算結果が与えられた定理の主張を裏付けることを示す試みである。1976年に示された四色定理が計算機援用証明によって示された最初の定理である。計算機援用証明は人工知能の分野でも使われ、簡明かつ陽的で新しい（数学の）定理の証明を作り出すことが目指された。このような自動定理証明機はいくつかの新しい結果を生み出し、既存の定理に対しても新しい証明を発見した。

手法[編集]

数学的証明の中でコンピュータを用いる方法の一つとして精度保証付き数値計算が挙げられる。これは数学的厳密さを保持したうえで数値計算を行うことを意味する。数値的プログラムの出力が与えられた数学的問題の解を含むことを示すために集合値演算などを使用する。これは区間演算などによって丸め誤差と打切り誤差を包含、伝播させることでなされる。より具体的には、数値計算を四則演算に簡略化する。計算機では四則演算の結果は計算精度に応じて丸められる。だが、四則演算の結果に関する上界と下界を与える区間を作ることができる。そして数を区間に置き換え、四則演算を計算機で表現可能な数で構成した区間で行う^[1]。

計算機援用証明で示された定理[編集]

四色定理^[2]
ケプラー予想^[3]^[4]
Double bubble 予想^[5]
Wright 予想^[6]
14番目のスメイルの問題、ウォリック・タッカーによって区間演算を使って解決された^[7]。
Robbins 予想（英語版）
Connect Four（英語版）
ブールピタゴラス数問題（英語版）^[8]

出典[編集]

^ ^a ^b 大石進一 et. al. (2018), 精度保証付き数値計算の基礎, コロナ社.
^ Appel, K., Haken, W.(1976) Every planar map is four colorable, Bulletin of the American Mathematical Society Volume 82, Number 5.
^ Hales, T. C. (2005). A proof of the Kepler conjecture. Annals of mathematics, 1065-1185.
^ Hales, T. et. al. (2017). A formal proof of the Kepler conjecture. In Forum of Mathematics, Cambridge University Press.
^ Hass, J., Hutchings, M., & Schlafly, R. (1995). The double bubble conjecture. Electronic Research Announcements of the American Mathematical Society, 1(3), 98-102.
^ van den Berg, J. B., & Jaquette, J. (2018). A proof of Wright's conjecture. Journal of Differential Equations, 264(12), 7412-7462.
^ Tucker, W. (1999). The Lorenz attractor exists. Comptes Rendus de l'Académie des Sciences-Series I-Mathematics, 328(12), 1197-1202.
^ Lamb, E. (2016). Two-hundred-terabyte maths proof is largest ever. Nature. 534: 17–18.

参考文献[編集]

Nakao, Mitsuhiro T; Plum, Michael; Watanabe, Yoshitaka (2019). Numerical verification methods and computer-assisted proofs for partial differential equations. Springer. doi:10.1007/978-981-13-7669-6
Meyer, K. R., & Schmidt, D. S. (Eds.). (2012). Computer aided proofs in analysis. en:Springer Science & Business Media.
Lanford, O. E. (1992). Computer assisted proofs. In Computational Methods in Field Theory (pp. 43-58). Springer, Berlin, Heidelberg.

外部リンク[編集]

計算機援用証明と精度保証付き数値計算 (PDF)

[oishi-1] 大石進一 et. al. (2018), 精度保証付き数値計算の基礎, コロナ社.

[2] Appel, K., Haken, W.(1976) Every planar map is four colorable, Bulletin of the American Mathematical Society Volume 82, Number 5.

[3] Hales, T. C. (2005). A proof of the Kepler conjecture. Annals of mathematics, 1065-1185.

[4] Hales, T. et. al. (2017). A formal proof of the Kepler conjecture. In Forum of Mathematics, Cambridge University Press.

[5] Hass, J., Hutchings, M., & Schlafly, R. (1995). The double bubble conjecture. Electronic Research Announcements of the American Mathematical Society, 1(3), 98-102.

[6] van den Berg, J. B., & Jaquette, J. (2018). A proof of Wright's conjecture. Journal of Differential Equations, 264(12), 7412-7462.

[7] Tucker, W. (1999). The Lorenz attractor exists. Comptes Rendus de l'Académie des Sciences-Series I-Mathematics, 328(12), 1197-1202.

[8] Lamb, E. (2016). Two-hundred-terabyte maths proof is largest ever. Nature. 534: 17–18.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

表話編歴数学
主要分野	数理論理学集合論圏論代数学初等線型多重線型抽象算術/数論解析学/微分積分学関数解析学行列解析幾何学代数微分有限離散位相代数的位相表現論リー理論（英語版）微分方程式線型微分方程式複素微分方程式常微分方程式偏微分方程式積分微分方程式力学系組合せ数学数理物理学ゲーム理論グラフ理論最適化問題数理最適化計算理論確率論数理統計学（英語版）制御理論三角法
トピックス	数学史和算算道数理哲学美未解決問題算数・数学教育算数教科
賞	ボッチャー記念賞コール賞フィールズ賞ヴェブレン賞サレム賞スティール賞ウルフ賞クラフォード賞クレイ研究賞ガウス賞アーベル賞ラマヌジャン賞 SASTRAラマヌジャン賞チャーン賞数学ブレイクスルー賞
応用	情報理論折紙の数学囲碁と数学数値解析精度保証付き数値計算計算機援用証明数値線形代数常微分方程式の数値解法偏微分方程式の数値解法
学会・団体	国際数学者会議国際数学連合国際産業数理・応用数理会議国際産業数理・応用数理評議会（英語版）アメリカ数学会 SIAM ヨーロッパ数学会ロンドン数学会日本応用数理学会日本数学会数学教育協議会
競技	国際数学オリンピック日本数学オリンピック日本ジュニア数学オリンピック広中杯近畿大学数学コンテスト人の最大の力を競う算数・数学の大会
研究所	京都大学数理解析研究所統計数理研究所アンリ・ポアンカレ研究所オーバーヴォルファッハ数学研究所クレイ研究所 CIMAT数学研究センターステクロフ数学研究所
一覧数学定数数関数図形数学記号数学者エポニムカテゴリポータル