数学の証明問題、長々とかかるものが解けたときってすごい達成感がありましたよね。ある数学者チームがものっっすごく長い証明を完成させたそうです。
どれだけ長いかって、データ量にしてなんと200TB（テラバイト）もあるそうです。
Natureによれば、テキサス大学オースティン校などの研究チームが、スーパーコンピュータで「ブールピタゴラス数問題」なるものを解くことに成功したそうです。
なんか字面を見るだけで難しそうな気がするんですが、どんなものかっていうと…
整数に赤または青の色を付けて、「a^2＋b^2＝c^2」となるようなa、b、cの組み合わせのすべての数が同じ色にならないようにすることは可能か？
そういえば中学校あたりで「3^2＋4^2＝5^2」って習ったような…こういう組み合わせになれる数を「ピタゴラス数」って言うんですね。
で、この問題は、ピタゴラス数の各数字を赤か青に振り分けて、組み合わせの中で全部同じ色じゃない状態を、全整数で作れるのかってことです。
え、それって「3＝赤」としたら4か5は青にする、ってだけですよね？ と一瞬思ったんですが、「全整数で」ってことだから、もっと大きいピタゴラス数まで同時に考えなきゃいけません。
たとえば「3、4、5」の次に大きいピタゴラス数は「5,12,13」で、「5」が共通しています。だから仮に「3＝赤」にしたら、4か5が青、じゃあさらに5が青だとしたら、12か13は赤…と、色の組み合わせが連鎖していきます。
この問題は数学者のロナルド・グラハムさんが1980年代に提起し、答えを見つけた人には100ドル（約1万1000円）がごほうびでもらえることになっていました。
今回問題を解いた研究チームはもうそれを受け取ったそうですが、1万円かぁ…。
で、肝心の答えは「ノー」。つまり、ピタゴラス数全部が同じ色にならないようにすることは全整数では不可能でした。
この結論に至るまでに、研究チームではピタゴラス数を7,825まで試していきました。
7,825になると、整数を色分けする方法は10²300;以上、数式でしぼっても1兆以上もあったそうです。ちなみに7,824までは答えはイエスで、こちらに実際どの数が何色になりえるかの図があります。
研究チームは数学的手法を使って多少効率化したものの、計算はテキサス大学のスーパーコンピュータStampedeの800個のプロセッサで2日がかりになりました。
そして作り出されたデータが、200TBにもなったんです。これまでの証明問題のデータ量で最大記録とされているのは2014年、13GBというものなので、一気に1万倍以上に増量したんですね。
こんな風にコンピュータの力技で証明問題を解く例が最近一般化しつつありますが、こういうやり方が本当に数学的証明といえるのかどうかについてはちょっと懐疑的な人たちもいます。
この件でも、たしかに「ノー」になるってことは実際の例で示せたんですけど、どうしてノーなのか、仕組みとしてはわからないままです。
とはいえ、今回の問題の計算量が人手ではとても無理という点では、議論の余地がなさそうです。
http://www.gizmodo.jp/2016/06/200tb.html