数学と計算機援用証明¶

はじめに¶

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

引用¶

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

— 古田彩 Aya FURUTA (@ayafuruta) 2013, 7月 15

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

— k u r i t a (@kuri_kurita) 2013, 7月 15

@kuri_kurita @ayafuruta 見破る方法は二つ、一つは独立した複数の実装、もう一つはソースコードの公開です。それぞれ、実験系での追試と生データの提供に相当しますね。

— Hiroyasu Kamo (@kamo_hiroyasu) 2013, 7月 16

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

— 古田彩 Aya FURUTA (@ayafuruta) 2013, 7月 15

@ayafuruta @kuri_kurita http://t.co/QYEEKiQ9gl 計算機援用証明というのがあるのですが，これ，今どのくらいあるのでしょうね．原理的に何がどこまでカバーできるのか凄く気になる所ですが

— 相転移P（市民） (@phasetr) 2013, 7月 15

@phasetr @kuri_kurita 計算機を援用することで、解（なのかな）の存在を「解析的に証明することに成功」というところが気になります。

— 古田彩 Aya FURUTA (@ayafuruta) 2013, 7月 16

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

— 古田彩 Aya FURUTA (@ayafuruta) 2013, 7月 16

@ayafuruta @phasetr @kuri_kurita 組合せ論的計算をゴリゴリ行う証明という意味で近いものとして、有限射影平面の探索があります。http://t.co/Oqj3zfyGEF

— Hiroyasu Kamo (@kamo_hiroyasu) 2013, 7月 16

@kamo_hiroyasu 色々と資料をご教示頂き，誠にありがとうございました。「ケプラー予想」は，amazonを見ると「数学の証明とコンピューターの関係について知りたいという方にオススメ」，しかも翻訳が青木薫さんということで，迷わず購入しました。

— 古田彩 Aya FURUTA (@ayafuruta) 2013, 7月 16

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

— 相転移P（市民） (@phasetr) 2013, 7月 16

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

— Hiroyasu Kamo (@kamo_hiroyasu) 2013, 7月 16

@phasetr @kuri_kurita 私の数学知識はご存知の通りですが、４色問題はすべての可能性をしらみつぶしに当たったものと理解していて、計算機援用証明ってそういうものだとばかり思っていました。「精度」保証による「解析的」証明が可能、というのは新鮮です。

— 古田彩 Aya FURUTA (@ayafuruta) 2013, 7月 16

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

— Hiroyasu Kamo (@kamo_hiroyasu) 2013, 7月 16

査読者情報を捏造した疑いで論文撤回というケースを依然見かけました…＞数学 RT @ayafuruta: 「測定」という裁判官がいない数学に、捏造は存在しないよなあ。人の成果を横取りするくらいしか思いつかないけど… http://t.co/7K4onT5VJJ

— 蟹 (@kanipuffin) 2013, 7月 16

@kany1120　おお、そんなことが。でもそれを捏造したとして、せいぜい結果の箔付けになる程度で、ウソの結論を同業者に信じさせることはできないですよねー。結果が合っているかどうかは、どうせ検証されちゃいます。捏造としては小物（笑）のような気がします。

— 古田彩 Aya FURUTA (@ayafuruta) 2013, 7月 16

Kepler 予想¶

Kepler 予想の本はこれだ.

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

ラベル¶

数学, 計算機援用証明, 数式処理, 精度保証, 有限射影平面, Kepler 予想