正しさをめぐる論争が、14年近く続く数学の証明がある。京都大学数理解析研究所の望月新一教授が2012年に公表した宇宙際タイヒミュラー理論(IUT)による「ABC予想」の証明だ。この予想は、いわば整数の世界における、足し算とかけ算の「奥深い関係」を表す根幹的な仮説であり、解決されれば多くの厄介な難問が一挙に解けるとされる。
天才数学者の証明とその後の波紋
望月氏は16歳で米プリンストン大に入学した俊英。数論幾何――「数を図形に置き換えて考える」というホットな分野――で、すでに重要な業績を出していた。世界中の数学者が驚き、注目したのも当然である。
ところが、その証明は合計500ページにも及び、斬新な概念や考え方が多数導入されていたため、理解できたとする数学者はごく少数にとどまった。同時に、批判を展開する数学者も現れた。影響が大きかったのは、ドイツの数学者ペーター・ショルツェ氏らによるものだ。ショルツェ氏は30歳で数学界のノーベル賞とも言われる「フィールズ賞」を受賞した、数学界の若きリーダーだ。彼は京都を訪れ、望月氏と直接議論したが、平行線をたどった。そして18年、IUTの定理3・11から系3・12を導く部分に深刻な問題があると指摘する報告書を公開した。
査読の異例の長期化と現状
一般に学術論文は、同分野の研究者による確認作業、「査読」を経る。数学論文の査読は長期化することもあるが、IUT論文は異例の7年半を要した。これを受けて有名な科学雑誌「Nature」は20年4月、「複数の専門家は、ショルツェ氏らの批判が出た時点で、この問題に決着がついたと見なしている」「論文誌への掲載が決まっても、それは変わらないだろう」と報じた。
現状、IUTによるABC予想の証明を、世界の数学界は認めていない。だが「数学的に正しい」とは、結局どういうことなのか。数学者の多数決で決まるわけでもないだろう。望月氏の論文は学術誌の正式な査読を通過したのも、また事実である。事態は膠着状態に陥った。
これに対し、打開策として始まったのが、定理証明支援システム「Lean」による検証プロジェクトである。証明をLeanに分かる言葉に書き換え(形式化)、論理の穴がないかを検査する試みである。
プロジェクトチームは今月1…
