コンピューター科学者のマライン・ヒュールは、挑戦しがいのある数学的課題がないか常に目を光らせている。カーネギーメロン大学（CMU）の准教授であるヒュールは、コンピューターを使って難解な数学問題を解決することに定評がある。2016年に発表した「ブールピタゴラス数問題」という証明問題の答えは、200TB（テラバイト）におよぶ数学証明問題の史上最大の解として、大きな話題となった。ヒュール准教授は現在、自動化アプローチを使って、あまりに単純なことで魅力的な「コラッツの予想」に取り組んでいる。
コラッツの予想とは、1930年代にドイツの数学者ローター・コラッツによって最初に提示された（というのが1つの説となっている）数論問題である。まず任意の正の整数をとり、その整数が偶数の場合は2で割り、奇数の場合は3を掛けて1を足すという操作を繰り返すと、生成される数列はどうなるか、というものだ。コラッツの予想では、数列は最終的に必ず1に到達する（そして、4、2、1を繰り返すループに入る）と主張されている。
たとえば、初期値が5の場合、次の6つの項しか生成されない：
5, 16, 8, 4, 2, 1
初期値が27の場合は、数列は111ステップにまで及び、周期的に増減を繰り返して最大9232にまで増大し、最終的に1に到達する。
40の場合も、短い数列を生成する：
40, 20, 10, 5, 16, 8, 4, 2, 1
コラッツの予想はこれまで、3垓（ がい、垓は10の20乗）くらいまでのすべての開始値について最終的に1に到達することがコンピューターで確認されている。
ほとんどの研究者はコラッツの予想が正しいと考えている。コラッツの予想には多くの数学者とそれ以外の人たちが惹きつけられてきたが、これまで証明できた人は皆無だ。1980年代初頭にハンガリーの著名な数学者であるポール・エルデシュは、「数学はまだこの種の問題に対する用意ができていない」と言明した。
「エルデシュはおそらく正しいと思います」とヒュール准教授はいう。ヒュール准教授にとってコラッツ予想の魅力は、解決の見込みよりも、自動推論手法の進歩にある。ヒュール准教授と彼の共同研究者であるスコット・アーロンソン教授とエムレ・ヨルクは、この問題に5年間取り組んできた。そして最近、プレプリント・サーバー「アーカイブ（arXiv）」に論文を投稿し、「私たちはコラッツの予想を証明することに成功していませんが、私たちのアイデアは興味深い新たなアプローチを示すものだと考えています」と述べている。
テキサス大学オースティン校のコンピューター科学者であるアーロンソン教授は、「尊い失敗です」と言う。コラッツの予想を証明できなかったので失敗ではあるが、別の意味で進歩したので尊いということだ。ヒュール准教授は今回の失敗を、人間とコンピューターのどちらがそのような問題を証明するのに優れているかを判断するための出発点になると考えている。
数学をコンピューター処理に変換する
多くの数学問題では、コンピューターは歴史的に蓄積されてきた膨大な数の研究を利用できないため、解決は見込めない。しかし、人間がお手上げなことでもコンピューターには得意な領域がある。コンピューターにターゲットと明確に定義された探索空間を与え、解のイメージを伝えれば、コンピューターはひたすら計算して解答を見つけることがある。もっとも、コンピューターの計算によって導かれた解が数学界に意義のある追加になるかどうかは議論の余地がある。従来の考え方では、人間の創造性と直感がもたらす概念やアイデアだけが数学領域を広げるとされ、コンピューティングによる進歩は工学的なものとして片付けられることが多い。
コンピューターとコラッツの予想はある意味、相性抜群だ。その理由の1つは、カーネギーメロン大学の論理学者で哲学教授のジェレミー・アビガッドが指摘するように、反復アルゴリズムの概念はコンピューター科学の基盤であり、コラッツの数列は決定論的なルールに従って段階的に進む反復アルゴリズムの一例であるからだ。同様に、あるプロセスが停止するのを示すことは、コンピューター科学ではよくある問題だ。「コンピューター科学者は一般に、アルゴリズムの実行が有限時間で停止すること、つまり、常に解を返すこと …