ABC予想の証明は達成されたか
今回は、ＡＢＣ予想の証明を巡って、望月新一教授の宇宙際タイヒミュラー理論について語る。
私は数学の専門家ではない。世界最高峰の数学者の論争を理解できるわけはない。
しかし、数学や物理の歴史を学ぶのは大好きで、論理の積み重ねと証明の構造でトップレベルの見解が真っ向から分かれる例として、現在数学界で起きているある壮大な論争に強く惹きつけられている。
京都大学数理解析研究所の望月新一教授によって構築された「宇宙際タイヒミュラー（IUT）理論」を巡る議論である。
今回は、数学の歴史に残るであろうこの理論と、その証明プロセスを巡る現状について、私の考えを整理してみたい。
足し算とかけ算の宇宙を繋ぐ「宇宙際」理論
宇宙際タイヒミュラー理論（Inter-universal Teichmüller Theory）とは、一言で言えば「かけ算の宇宙」と「足し算の宇宙」という、本来交わらない別々の数学的世界を繋ぐための理論である。
だからこそ「宇宙際（インター・ユニバーサル）」と呼ばれる。
この理論の最大の目的は、整数論における超難問「ABC予想」を証明することにあった。
ABC予想とは、簡潔に言えば「互いに素な自然数 a, b, c が a + b = c を満たすとき、c の大きさは a, b, c の素因数の積（rad(abc) と呼ばれる）によって本質的に抑えられる」という予想である。足し算とかけ算（素因数分解）の間の根源的な関係を提唱しており、この予想が証明されれば整数論の多くの難問が一気に解決されるとされる。
望月教授は2012年8月にインターネット上で4編・計600ページを超える論文を発表した。
その後、実に8年近い異例の長期にわたる厳しい査読を経て、2021年3月に京都大学の専門誌『PRIMS（Publications of the Research Institute for Mathematical Sciences）』にて正式に公刊された。
しかし、事態はすんなりと進んでいない。
2018年には、数学界のノーベル賞と呼ばれるフィールズ賞を受賞したピーター・ショルツェ教授（ボン大学、ドイツ）と、ヤコブ・シュティックス教授（フランクフルト大学、ドイツ）が連名で、「証明の重要な部分に論理の飛躍（ギャップ）がある。特定の条件下で同一視できる場合ではないものを同一視しており同一視として成立しない、あるいはトートロジー（同義反復）に陥っている」と批判の声を上げた。
これに対し望月教授は、「批判者たちは、IUT理論が構築した『別々の数学的宇宙のずれを修正し、比較する』という根本的な構造を理解しておらず、既存の単一の宇宙の中だけで物事を解釈しようとしている」と再反論した。
現在も数学界では議論が膠着状態にある。
そこで現在提唱されているのが、証明支援プログラミング言語「Lean（リーン）」を用いたアプローチである。
人間の頭脳や直感による解釈の相違を排除し、論理のステップをすべてプログラム言語に書き換えることで真偽を検証しようという試みであり、望月教授自身も、当初は疑問を呈しながらも、現在はこれに賛同している。
群論、楕円曲線、そしてフェルマーの最終定理へ
なぜ「足し算とかけ算の関係を解明する」ことが、それほどまでにおおがかりなことになるのか。
それを理解するために、誰もが一度は耳にしたことがある「フェルマーの最終定理」の証明プロセスと、そこに至る数学の系譜を振り返ってみたい。
x^n + y^n = z^n
「n が3以上の整数のとき、これを満たす自然数 x, y, z の組は存在しない」。これがフェルマーの最終定理である。
n=2 の場合（x^2 + y^2 = z^2）は、高校数学でもおなじみの三平方の定理（ピタゴラスの定理）であり、3:4:5 などの無数の整数解（ピタゴラス数）が存在する。
なお、n=2 の方程式 x^2 + y^2 = z^2 は円を定義するが、楕円曲線とは別の概念であることに注意が必要である（楕円曲線は後述するように y^2 = x^3 + ax + b の形で定義される代数曲線である）。
しかし、これが3乗、4乗となると、途端に整数解が存在しなくなる。
この問題に対し、過去の天才数学者たちが個別に取り組んで証明してきた。
・n=4 はフェルマー自身（1640年頃）
・n=3 はレオンハルト・オイラー（1770年）
・n=5 はディリクレやルジャンドル（1825年）
といった時系列である。
しかし、すべての n で証明されるまでには、350年以上の時間を要した。
ここで重要な背景となるのが「群論」である。
群論とは、19世紀初頭にエヴァリスト・ガロアが提唱した数学の一分野で、「対称性の構造」を代数的に研究するものである。
ガロアは若くして決闘で命を落とすが、その遺した理論（後の「ガロア理論」）は、数式の根（解）がどのような対称性の構造を持つかを群として記述し、方程式の解の可能性を根本から問い直すものだった。
群論はその後、整数や有理数・複素数など「数の体系」の構造研究と結びつき、数論（整数論）の根幹をなす道具となった。
さらに20世紀には、アーベル群（可換な群、すなわち演算の順序を入れ替えても結果が変わらない群）の構造論が代数幾何学と融合し、整数論研究の強力な基盤となっていく。
なお「アーベル群」の名称は、19世紀ノルウェーの数学者ニールス・ヘンリク・アーベルに由来する。
アーベルはガロアとほぼ同時代の人物で、5次以上の方程式が代数的に解けないことを証明したことで知られる。群論の可換性の概念と彼の名前が結びつき、後世「アーベル群」と呼ばれるようになった。
ガロアもアーベルも、20代という短い生涯の中でこれだけの仕事を残した。
この、数を因数分解するということは、本質的に「かけ算」の世界の出来事である。
しかし方程式には「足し算（＋）」が組み込まれている。
かけ算の世界に足し算を持ち込むと、とたんに要素が複雑に絡み合い、もとの数の素因数の性質が遡って追えなくなってしまう。
これは「かけ算の宇宙が、足し算の宇宙によって破壊される現象」と言われる。
この整数の世界における破壊現象を「楕円曲線（y^2 = x^3 + ax + b という形の方程式が描く曲線）」という幾何学的な形に落とし込み、その性質・対称性をアーベル群の構造として研究することで解明したのが、1995年のアンドリュー・ワイルズによるフェルマーの最終定理の証明プロセスであった。
ワイルズの証明は、「楕円曲線のモジュラー性」（谷山・志村予想）によって証明するという迂回路をたどったもので、その中心にあったのは楕円曲線のガロア表現という理論である。
なお、「谷山・志村予想」の「谷山」は日本人数学者・谷山豊（1927-1958）であり、彼もまた31歳で夭折した。ガロア、アーベル、谷山、この分野の歴史は、若くして世を去った天才たちの仕事の上に積み重ねられている。
アレクサンドル・グロタンディークから望月教授へ
望月教授のIUT理論は、この「数の破壊現象」をさらに根源的に捉え直す。
破壊された結果から生じる「ずれ」がどの程度のものなのかについて、別々の宇宙（足し算の宇宙とかけ算の宇宙）を、群論の写像、圏論の射、関手、さらにはテータ関数その他の望月教授が築いたもろもろの新しい数学概念によって関係性を構築し、繋いだときのずれの範囲を解析し、ABC予想にいう不等式を満たす自然数の組がたかだか有限になることを導く理論である。
この理論の背景には、20世紀最大の数学者の一人と呼ばれるアレクサンドル・グロタンディーク（フランス）が提唱したスキーム理論・トポス理論といった代数幾何学の枠組みがある。
グロタンディークは「数学の対象そのものよりも、対象の間の関係性（射）を研究せよ」という思想で代数幾何学を根本から作り直した。代表的な概念が「圏論（Category Theory）」である。
圏論とは、数学的対象（群、環、空間など）をそれ自体としてではなく、対象と対象の間の「射（morphism）」の構造として捉え直す理論である。
グロタンディークはこの圏論の言語を用いて代数幾何学を再構成した。
IUT理論もまた、この圏論的な「射による解析」と群論の写像を組み合わせながら、異なる数学的宇宙の間の関係性を記述するフレームワークを構築している。
また、グロタンディークは「グロタンディーク宇宙」という概念を導入した。これは、通常の集合論（ZFC公理系）を拡張し、「数学的操作を閉じた状態で行える十分に大きな集合の宇宙が存在する」という公理（宇宙公理）を追加するものであった。
圏論において「すべての集合の圏」を扱おうとすると、ラッセルのパラドックスに類する論理的矛盾が生じる。グロタンディーク宇宙の公理は、その問題を回避するための基礎として、現代の代数幾何学・圏論における大きな枠組みとなっている。
IUT理論はこのグロタンディーク宇宙の公理をフレームワークの根幹として使用している。
グロタンディーク宇宙の存在（より正確には、「到達不可能基数」と呼ばれる特別な無限の存在）は、通常のZFC集合論の公理系の中では証明も反証もできないことが知られている。これはゲーデルの不完全性定理の射程内にある問題であり、より強力な公理を追加することによってのみ宇宙の存在を保証できる。
なお、フェルマーの最終定理のワイルズによる証明もグロタンディーク宇宙の公理を使用しているが、その後の研究によって、グロタンディーク宇宙の公理を使わない通常のZFC集合論の範囲内でも証明できることが確認された。一方、IUT理論は根幹においてグロタンディーク宇宙の公理の枠組みに依拠して構築されている。
そのグロタンディークが1980年代に提唱したのが「遠アーベル幾何学（Anabelian Geometry）」という研究である。
これは、「代数曲線の幾何学的な情報は、その根本にあるガロア群（アーベル群を超えた、より複雑な非可換な群）によって完全に復元できるのではないか」という予想を中心とする分野である。
名称の「遠（anabelian）」とは「アーベル群からほど遠い（非可換な）」という意味である。
日本は伝統的にこの遠アーベル幾何学の研究で世界をリードしており、その先端を切り拓いてきた第一人者が望月教授である。
すなわち、フェルマーの最終定理の証明とIUT理論にはそれぞれ次のような数学理論の系譜がある。
群論（ガロア）→ 代数幾何学（グロタンディーク）→ 楕円曲線・モジュラー形式・ガロア表現 → ワイルズによるフェルマーの最終定理の証明
群論（ガロア）→ 代数幾何学（グロタンディーク）→ 遠アーベル幾何学（グロタンディークの提唱、望月教授らが発展）→ IUT理論（足し算とかけ算の宇宙を繋ぐ）
系譜に近縁性があり、証明のアプローチとしてはスジがよさそうに思える。
IUT理論が前提とするABC予想が完全に証明されれば、フェルマーの最終定理は別ルートから非常にシンプルかつ強力に証明できる。但し小さな n については別途確認が必要となる。
争点となる「系3.12」と、Leanによる形式検証
現在、批判者たちが「ギャップがある」と指摘しているのは、IUT理論の論文第3巻にある「系3.12（Corollary 3.12）」と呼ばれる部分である。
ここが、かけ算の宇宙と足し算の宇宙を繋ぐ最終段階、最重要なリンクに当たる。
批判者側は、このリンク部分において「IUT理論がかけ算の世界の定数と別の世界の定数を同一視している箇所が同一視できないものを同一視しており論理が飛躍している（ギャップがある）か、トートロジーである」と主張する。IUT理論にいう3つの不定性が大きければ、射や関数による変換の繰返しにより宇宙際のずれは拡がりすぎて、ずれを比較する解析として成立していないという批判である。
一方、望月教授は「彼らはIUTが積み上げてきた『別々の宇宙の定数を比較するための長大なプロセス』を無視し、既存の単一の宇宙のルールに無理やり当てはめようとしている」と反論する。
興味深いのは、批判者側も、「それが数学的エラーである」ことの決定的な証明（反例の提示など）には至っていないように見える点である。
なお、証明責任が証明者側にあることはもちろんである。
また、「系3.12」（系3.11から系3.12を導くプロセス）以外の膨大な理論構築プロセスについては、目立った批判が存在していない。
つまり争点は、「系3.12以外の圧倒的なボリュームの証明プロセスが、系3.12で比較される2つの定数をリンクさせるために、正しく機能しているか否か」に絞られていると言えるだろう。
Leanによる「形式検証」の挑戦
ここで登場するのが、先述した証明支援言語「Lean」を用いたプロジェクトである。
東京工業大学（現・東京科学大学）の加藤文元教授（『宇宙と宇宙をつなぐ数学』著者）なども紹介している通り、IUT理論の全プロセスをLeanに書き換える作業が進んでいる。
LANA プロジェクト発表にあたって
https://zen.ac.jp/zmc/topics/jwz-o8xr3v6f
がわかりやすい。
法律や契約書の世界でも、曖昧な解釈を許さないために定義を厳密化するが、数学の証明をコード化することは、論理の厳密化の究極形と言えるだろう。
Lean で行うのは、数学的命題を「型（Type）」として表現し、その「証明」を「その型の値を構築するプログラム」として記述するという、「型理論（Type Theory）」に基づく形式化であり、命題「AならばBである」は「A型の値が与えられたとき、B型の値を返す関数」として表現され、コンパイラがその論理的整合性を機械的に検証する。
IUT理論は、望月教授がほぼ独力で構築した全く新しい数学的なフレームワークであり、数百ページにわたる膨大な論文であり、世界の数学者でも理論として全体像を理解できている人間は極めて少ないとされている。
Lean（と数学的定理のライブラリのMathlib）に入力するためには、理論内で使われている「既存の定理」も含めて遡ってすべて真であるところまでの証明プロセスを記述していく必要がある。
２つの世界の定数が別物というなら、定数の種類も複数段階で設定され、定義によって厳密に使い分けられ、複数の定数がどう関係するのかもまた関数や定義により区別して記述されなければならない。
この定数というのは、プログラミング的に言えば変数で、ローカル変数を他のルーチン内の変数と同一視してはいけない、グローバル変数が使えない場面で使うようなことをしてはいけない、というような意味合いになるだろう。
その遡行作業と拡張のボリュームは途方もないものになるだろう。
リンクは繋がっているか
IUT理論の成否は結局のところ、「別々の宇宙を繋ぐリンクの、最後の一つの輪っか（定数の比較）が、正しく結合されているか否か」にかかっているだろう。
数学者ではない私としては、根拠のない直感にすぎないが、事の経緯を見るに、私は「最後の一つの輪は繋げることに成功しているものの、そこに至るまでの長大で全く新しいフレームワークが、未だ超一流の数学者たちにさえ正しく組み込まれていない状態」なのではないかと考えている。
Leanによる検証という、一切の人間的解釈を削ぎ落とした検証は、いったいどのような結末をもたらすのだろうか。
果たしてLeanによる形式化は、成功するのか。
Lean（とMathlib）に基づいて形式化された結果、成功・失敗の判定が出たとして、その判定コード自体にバグ（ギャップ）がないのかをまた再検証するというステージに入るように思われる。
そして、デバッグのプロセスにおいて、またLeanに落とし込む過程において、証明の補完、または数学的表現の補完がなされて、IUT理論は「真」であるとして、ＡＢＣ予想の証明が完成するのかもしれない。私はその可能性が結構大きいと思っている。
そして、そのLeanで書かれたコードの数学的な整合性そのものを、人は、そしてLeanは検証できるのだろうか。
それには終わりがあるのだろうか。
この問いは、「形式化された数学的述語の公理系において、証明を検証するシステム自体の正しさは、どう保証するのか」——という、20世紀初頭からゲーデルの不完全性定理をめぐって議論されてきた深い問いと、どこか重なっているようにも思われる。
Lean が依拠する型理論の体系は、数学的に健全（Sound）であることが証明されているというが、それもまた、ある公理系の上に立った証明であることに変わりはない。
もし「系3.12が当該の公理系において真として成立する」としても、それはその公理系の上での真であって、望月教授の構築したいくつかの数学的概念を所与のものとして使用しない（数学的感覚として踏まえられない）者にとっては、どこまでも証明が成立していないように見える可能性も、原理的に排除できない。
私見であるが、ショルツェ教授の、「同一視できないものを同一視している」という批判に対しては、望月教授がおこなった群の写像や、ホッジ・アラケロフ、テータ・log格子などの変換作業やその度に変数（定数）に付される多種多様な符号（ラベル、カプセル化）が論理的整合性をもって逐一たどれるのであれば、それぞれの変換の段階での変数（定数）は混同されておらず、遠アーベル幾何学における群や圏の変換において「構造」は堅固に維持されるはずであり、宇宙際の写像によりその構造がぼやけるとしてもその構造のぼやけは解析可能だという再反論は、首肯すべきものがあるように思われる。
しかしグロタンディーク宇宙における集合や圏は無限に近いような素数の集まりでありあまりに巨大な数学的対象であるから、その構造がぼやけるのであれば数学的に意味をなさないランダムな素数の集まりでしかない、という数学的感覚が、ショルツェ教授らの批判の根底にあるように思われる。
ショルツェ教授は、宇宙際タイヒミュラー理論を簡略化したものを提示して、宇宙際を跨いだぼやけが無限大に拡がると批判したということであるが、ラベルやカプセルを簡略化した計算結果をもって宇宙際のぼやけが無限大になるという批判が果たして批判として噛み合っているのかとも思われる。もちろん、簡略化した計算結果が同様に妥当する可能性もあるので、ことは単純ではないが。
一方、望月教授は、グロタンディーク宇宙における巨大な群や圏の構造は様々な変換をおこなっても固いものであり、宇宙際に写像として投影した場合はぼやけているが構造のぼやけの範囲は数学的対象が巨大であろうと否とを問わず解析可能である、と考えているように思われる。
望月教授はショルツェ教授らとの論争について、批判者はIUTの証明プロセスを従前の数学的感覚で不当に簡略化したものを措定してそれによれば証明が成立していないと言っている、と批判している。
つまり望月教授によれば、論理にギャップがあるのはショルツェ教授らによる批判の方であるというものである。
そして、ショルツェ教授らの、3つの不定性によるずれにより2つの宇宙間のずれが拡がりすぎて比較不可能になっているという指摘は、IUT理論の形式化によってIUT理論自身によって反駁・検証することは可能であろうか。
ショルツェ教授が簡略化した論理を形式化すれば証明不成立となり、望月教授の論理を形式化すれば証明成立となる可能性も十分にある。それをどう評価すべきか。
望月教授のブログ
https://plaza.rakuten.co.jp/shinichi0329/
によれば、
・宇宙際タイヒミューラー理論の原論文4編の第4論文[IUTchIV]の§3で解説している関手的アルゴリズムのspecies（種）/mutations（突然変異）という概念がLeanではまだ形式化・定義がされていない。しかしspecies/mutationsは新規性のある話でも難しい話でもなく数理研の90年代半ば以降の遠アーベル幾何全般において多くの数学者が無意識にこなしている処理であり、非常に基本的な立ち位置にある。
・species/mutationsの理論において本質的な役割を果たす「不定元のような論理式」（＝特定されていない、「とある論理式Φ」のようなもの）を扱うには、一階述語理論としてのZFCが必要であり、それはMathLib上ではまだ実装されていない
・speciesが定まり、speciesの対象からなる「圏」が定まり、圏の間の「関手」が定まるので、species/mutationsの形式化をする方が純粋数学の感覚との相性・整合性においてLeanで既存で実装されているtype/dependent functorより遥かに高い
・IUT理論への批判者たちは、speciesに深く関係している箇所、具体的には貼り合わせデータに登場する群の扱いを、誤ってIUT理論の扱いと異なるものとして扱っている、あるいはspecies的な考え方を無視している。
ということである。
つまり、Leanにおいては遠アーベル幾何学やタイヒミュラー理論の数学的述語が実装されておらず、遠アーベル幾何学やタイヒミュラー理論の外部にいる数学者においては数学的述語として正しく扱われていない、ということであり、なんとなく、何が起きているのかは見えてきたようである。
IUT理論のLean実装においても、遠アーベル幾何学の形式化が先行して進められているということのようである。
もう一人注目すべき数学者がいる。アリゾナ大学のキルティ・ジョシ（Kirti Joshi）教授である。
ジョシ教授は「算術的タイヒミュラー理論（Arithmetic Teichmüller Theory）」という独自の枠組みを構築し、2024年から2025年にかけて論文を精力的に発表している。
その中には「系3.12の証明」と「ABC予想の証明」を標榜するものがあり、さらに望月教授のIUTとジョシの理論の対応を示す「ロゼッタ・ストーン」論文も発表されている。
ただし、望月教授・ショルツェ教授の双方からジョシ教授の論文への批判も出されており、ジョシ教授自身も修正を重ねながら議論を続けている。
ジョシ教授の算術的タイヒミュラー理論が将来Leanによって記述されたとき、その補足証明は真と判定されるのかどうか。
あるいは、さらに別の証明の補足が提唱されるのか。それがLeanへの実装の過程で記述されるのか。
これもまたこの分野の興味深い論点の一つである。
この公理系の構造は、やや古典的だが、19世紀の非ユークリッド幾何学をめぐる問題とも共鳴する。
ユークリッドの「平行線公理（第5公準）」は長らく「他の公理から証明できるはずだ」と信じられてきたが、19世紀になって、この公準は他の公理からは独立であること、すなわち、これを否定しても矛盾は生じないことが証明された。
こうして「平行線公理のない幾何学」（非ユークリッド幾何学）が無矛盾な数学体系として成立し、どちらが「真の幾何学」かは、数学の問題ではなく、空間という物理の問題になることが明らかになった。
つまり、公理系の「正しさ」はその体系の内部では保証できず、外側から問うしかない——という構造は、Leanによる検証もまた、根底にはらんでいる可能性がある。
それでも、Leanによって記述された公理系においてもしIUTが真と証明されるとなれば、それはその公理系に基づく証明として成り立っていることになる。
機械による形式検証は、少なくとも「人間の数学的感覚のズレ」という最大の障壁を取り除く強力な手段である。
古典的力学に対する量子力学の登場においても、いわば、それぞれある条件下で両立するはずの公理系の違いが、物理学者の間でも感覚の許容範囲を超えて激しい対立を引き起こした。
量子力学の波動関数からウィグナー関数における量子の確率分布や構造化の理論は、宇宙際タイヒミュラー理論の宇宙間写像のぼやけの範囲の解析、構造の絞り込みの理論と、なにか近いものを感じるのは私だけだろうか。
IUT理論とくにホッジ・アラケロフ空間の理論は、遠アーベル幾何学に基づいて、ヴェイユ予想（有限体上に限ってリーマンゼータ関数が妥当することを証明した）に通じる結果を無限次元において導いており、将来的にリーマン予想（ディリクレのL関数）の解明のツールになりうる、という指摘もされている。
手近なところとしては、LeanやMathlibのソースにおいて、「真か偽か」の分岐の中で、「写像のぼやけの範囲を計測する、補正する」などという関数をどのようにプログラミングするのか、それだけでも興味がつきない。
IUT理論の論争によって数学の概念が変わる（変わった）のかもしれないし、変わらないのかもしれないし、変わるにはまだ100年くらいかかるのかもしれないなとも感じる。
現時点での私の観測は「IUT理論は最終的に真と証明されるだろう」（数学的述語の修正や補足証明はありうるとして）という見方である。
この壮大な数学の歴史におけるドラマの結末を引き続き見守っていきたい。