計算機援用証明

微分方程式
ナビエ–ストークス方程式。障害物の周囲の気流のシミュレーションに用いられる。
ナビエ–ストークス方程式。障害物の周囲の気流のシミュレーションに用いられる。
分類
タイプ
変数のタイプにより
  • 独立変数と従属変数（英語版）
特徴
過程との関係
  • 差分 (離散類似)
  • 確率
    • 確率偏（英語版）
  • 遅延（英語版）
解
一般的な話題
  • 表
  • 話
  • 編
  • 歴

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

手法

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

計算機援用証明で示された定理

出典

  1. ^ a b 大石進一 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.

参考文献

  • 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. https://link.springer.com/book/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)
  • 表
  • 話
  • 編
  • 歴
有限差分法
放物型偏微分方程式
  • FTCSスキーム（英語版）
  • クランク・ニコルソン法（英語版）
双曲型偏微分方程式
  • ラックス・フリードリヒ法（英語版）
  • ラックス・ウェンドロフ法（英語版）
  • マコマック法（英語版）
  • 風上スキーム（英語版）
  • 特性曲線法
その他
有限体積法
  • ゴドノフスキーム（英語版）
  • 高分解能スキーム（英語版）
  • 保存法則用単調性上流中心差分スキーム（英語版）
  • 移流上流分離法（英語版）
  • リーマン解法（英語版）
有限要素法
  • hp-FEM（英語版）
  • 拡張型有限要素法（英語版） (XFEM)
  • 不連続ガラーキン法（英語版） (DG)
  • スペクトル要素法（英語版） (SEM)
  • モルタル有限要素法（英語版）
メッシュフリー法・粒子法
  • SPH法
  • MPS法（英語版）
  • MPM法（英語版）
領域分割法
  • シューア補元法（英語版）
  • 仮想領域法（英語版）
  • シュヴァルツ交代法（加法シュヴァルツ法（英語版）・抽象加法シュヴァルツ法（英語版））
  • ノイマン・ディレクレ法（英語版）
  • ノイマン・ノイマン法（英語版）
  • ポアンカレ・ステクロフ法（英語版）
  • バランシング領域分割法（英語版） (BDD)
  • BDDC法（英語版）
  • FETI法（英語版）
  • FETI-DP法（英語版）
その他
  • 表
  • 話
  • 編
  • 歴
主要分野
トピックス
賞
応用
学会・団体
競技
研究所