計算機援用証明
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2024/03/14 01:55 UTC 版)
計算機援用証明とは、コンピュータによって少なくとも一部が生成された数学的証明である[1]。 今日における計算機援用証明のほとんどは数学的定理に対するしらみつぶし法の実装である。具体的には、膨大で複雑な計算をコンピュータによって実行し、計算結果が与えられた定理の主張を裏付けることを示す試みである。1976年に示された四色定理が計算機援用証明によって示された最初の定理である。 計算機援用証明は人工知能の分野でも使われ、簡明かつ陽的で新しい（数学の）定理の証明を作り出すことが目指された。このような自動定理証明機はいくつかの新しい結果を生み出し、既存の定理に対しても新しい証明を発見した。
- ^ 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.
[続きの解説]
「計算機援用証明」の続きの解説一覧
- 1 計算機援用証明とは
- 2 計算機援用証明の概要
- 3 手法
- 4 外部リンク
- 計算機援用証明のページへのリンク
