数学と計算機援用証明

古田彩さんのこんな呟き があり, そこに反応したら鴨さんからのリアクションまで返ってきて戦慄したのでメモしておく.

「測定」という裁判官がいない数学に, 捏造は存在しないよなあ. 人の成果を横取りするくらいしか思いつかないけどhttp://ow.ly/mZDuE 

@ayafuruta 四色問題のように, コンピュータを使った証明でプログラムに細工をしてしまうとか… 

@kuri_kurita なるほど. しかし生物や物理の実験データ捏造より, 簡単にバレそうですねー. 「お前は実験が下手だから再現できないんだ」という強弁が通らないので. 

@ayafuruta @kuri_kurita http://www.math.kobe-u.ac.jp/a-prize/jusho3-3.html 計算機援用証明というのがあるのですが, これ, 今どのくらいあるのでしょうね. 原理的に何がどこまでカバーできるのか凄く気になる所ですが 

@phasetr @kuri_kurita へー, 四色問題方式って, その後もこんな風に発展していたんですね. 知りませんでした. 教えて下さってありがとうございます. 

@ayafuruta @kuri_kurita 歴史的な経緯は全く知らないのですが, 私の知る限り 4 色問題は厳密に処理できる数式処理などの系統であって, 微分方程式は精度保証周りで意識が大分違う感じはします. 素人なのでアレですが, 前者は代数周り, 後者は解析周りという印象 

@phasetr @ayafuruta @kuri_kurita 数理計算をゴリゴリ使った証明といえば, 古くは, 整面凸多面体の決定 (Zalgaller 1966) があります. 

@ayafuruta @phasetr @kuri_kurita ケプラー予想の解決 (Hales 1997) も精度保証計算を利用した証明です. 啓蒙書も書かれています. 

@ayafuruta @phasetr @kuri_kurita 組合せ論的計算をゴリゴリ行う証明という意味で近いものとして, 有限射影平面の探索があります. http://mathdl.maa.org/images/upload\_library/22/Ford/Lam305-318.pdf

Kepler 予想の本はこれだ.

鴨さんからご紹介頂いた文献も読みたいが, 積読がたまる一方でつらい.