ジョージ・G・スピーロ「ケプラー予想」
コマネチ大学数学科でも登場した、充填問題。球を効率よく詰め込むにはどういう並べ方が一番よいか？ 約400年前、ケプラーは果物屋でのみかんの積み方が一番だと予想した。しかし、それが数学的に厳密に証明されたのは1998年のことだった……
一応、証明されたにもかかわらず、いまだに「予想」であるところがひとつの読み所になっている。
この手の本が楽しいのは、登場する数学者がとにかく大物揃いであるということだ。400年近くも数学者の頭を悩まし続けた問題であるだけに、メジャーな数学者だけとっても、ケプラーから始まり、ラグランジュ、ニュートン、ガウス、ヒルベルト……とオールスターである。オイラーは直接はからまないものの、彼が発見したグラフ理論の定理は何度も登場する。
また全体の雰囲気としては「フェルマー最終定理」よりは、オチも含めて「四色問題」に近い。つまりワイルズがやったみたいに、アクロバットな跳躍から見事な証明をしてみせたというわけではないのだ。泥臭い作業をコンピュータを使ってこつこつとやった結果、とりあえず証明できたみたいだけど何か？という感じなのである。それが証拠に、証明に使われた数学上のテクニックも（本書を読む限り）それほど高度ではない。
それでもプログラムに間違いがない限り、証明されたことは間違いないといっていいだろう。とはいえコンピュータがはじき出したデータは膨大で、とてもじゃないが人間がいちいちチェックできる量ではない。そのため査読チームは「証明が正しいことは99％まで確信できたが、完全なる確信には到達できなかった」と語っている。いまだ「定理」にはなっていないのだ。
コンピュータによる証明には問題点が二つある。
1.ＣＰＵが間違いを犯す可能性が否定できない
2.それで証明できたとして一体何がわかったと言えるのか
ということである。
１に関しては、いまどきコンピュータより計算が得意という人間はいないだろうし、複数のコンピュータ、複数の言語で確かめればまず間違いないだろう。
問題になるのは２のほうだ。つまり数学的意味、学問的価値が問われてくるのである。
たとえばどんな数学的問題にも真偽で答えてくれるコンピュータがあったとしよう（不完全性定理のことはおいとくとして）。それにフェルマーの最終定理が正しいかどうか訊ねたところ真であったとする。もちろん今では証明されているので真に決まっている。しかし、手探り状態だった遙か昔に、この問いかけをしたならどうだろう？ 真であっても偽であっても、だから何？という気分になるだろう。この定理を利用して、次のステップに行くことはできるかもしれないが、なぜフェルマーの最終定理が正しいかどうかということはサッパリわかっていないのだから。そして数学者たちはなぜ真になるのかという探求に心血を注ぐことに変わりないだろう。
ようするに俺ってばスゲー感がゼロで、全然ありがたみがないわけだ。
となるとコンピュータによる証明の問題は、数学と言うよりは人間の認識や論理の受け止め方に対するスタンス、つまり哲学の問題になってくるのではないだろうか。むしろ数学畑だけではなく、広い視野で検討してゆく必要があるだろう。そういうテーマの研究も面白そうだ。
余談
なにげにケプラーの人柄の話が面白かった。やっぱ月旅行小説まで書いちゃう人はハジけている。
