前回の続き
前回、私は「宇宙際タイヒミュラー理論とLeanによるABC予想の証明の試み」という記事を書いた（2026年6月9日）。
https://lawfield.com/blog/2026/06/09/3126/
そこで私は、数学者ではない者の直感にすぎないが、かなりの時間を要するとしても、Leanへの実装の過程で数学的述語の補足や補足証明がなされ、IUT理論によるABC予想の証明は最終的に「真」と証明されるだろう、その可能性は結構大きいと思っている、と書いた。
その約1か月後、動きがあった。
京都大学数理解析研究所の望月新一教授が提唱したIUT（宇宙際タイヒミュラー）理論を、証明支援系Leanで形式化し検証しようとするLANAプロジェクトが、2026年7月17日、初めての中間報告を公開したのである。
プロジェクトのメンバーによる記者会見が、祇園祭の前祭の巡行が終わった時間から、YouTubeやニコニコ動画などで中継された。
しかし重要なのは、中間報告書全文（英語。日本語版はたぶん無し）のほうである。
ZEN大学・ZMC（ZEN数学センター）のプレスリリース https://zen.ac.jp/news/zmcpostevent0717
報告書全文（PDF） https://github.com/katobungen/LANA_report_202607/blob/pdf/LANA_report_202607.pdf
プロジェクトリーダーは、前回の記事でも触れた加藤文元教授（『宇宙と宇宙をつなぐ数学』の著者、現在はZEN大学教授・ZMC所長）である。コアメンバーには、Johan Commelin、Kiran Kedlaya、Adam Topaz、そしてIUT理論の第一人者のひとりである星裕一郎氏（京大数理研）が名を連ねる。LANAとは「Lean for ANAbelian geometry（遠アーベル幾何学のためのLean）」の略だという。
その結論は、控えめに言っても、楽観的な見通しとはいえないものだった。
中間報告の結論は、「保留」である。
報告書とプレスリリースが述べている結論を、私なりに要約すればこうなる。
現時点でLANAプロジェクトは、IUT理論によってABC予想の証明が得られたか否かの判断を保留する。数学的なギャップが存在する可能性は排除しないが、それが本当にギャップなのか、それともまだLANAメンバーの理解が十分に深まっていないことに由来するのかについても、最終的な判断を保留する。今後も望月氏との対話を続けながら、独立した検証を継続する。
というものである。
つまり「証明は成立した」でも「証明は間違っている」でもない。「まだ分からない」である。そして、その「分からなさ」の中心には、Leanによる形式化作業が突き当たっている一つの「壁」がある。
前回の私は、「最後の一つの輪は繋げることに成功しているものの、そこに至るまでの長大なフレームワークが、未だ超一流の数学者たちにさえ正しく組み込まれていない状態」なのではないか、と書いた。
ところが中間報告書の原文を読む限り、事態はもっと手強い。問題は「最後の一つの輪」そのものにあり、しかもその輪をLeanのコードとして書き下すことに、プロジェクトはかなり難渋しているように見える。
そこで私は、報告書の該当箇所を、ClaudeとGoogleのGemini Notebookという二つのAIに読み込ませて対話しながら、この「壁」の正体を自分なりに掘り下げてみることにした。
以下は、その対話から私が理解した限りのことの整理である。例によって、私は数学の専門家ではない。誤解があれば、それは私の理解と説明能力の欠如が原因である。群論や圏論などの専門用語も飛び交うが、私は本質のところまでは理解できていないまま、AIと対話した中身として解説していることをご容赦いただきたい。
争点はどこにあるか──「系3.12」
前回の記事でも書いたとおり、批判者たちが「ギャップがある」と指摘してきたのは、IUT理論の第3論文にある「定理3.11から系3.12（Corollary 3.12）を導く過程」である。ここが、かけ算の宇宙と足し算の宇宙を繋ぐ最終段階、最重要のリンクにあたる。
LANAの報告書も、まさにこの一点に照準を絞っている。そして報告書は、この問題を、私のような素人にも、輪郭だけは掴める形にまで「翻訳」してくれている。それ自体が、この中間報告の功績だと思う。
報告書によれば、争点は最終的に、「q-パイロットの対数体積（-|log(q)|という一つの実数）を計算する二つの方法が、一致すると言えるかどうか」という問題に還元される。
ひとつ目の計算は、その宇宙に本来備わっている環構造（ふつうの足し算・かけ算の構造）を使って、素直に -|log(q)| を計算する方法。
ふたつ目の計算は、Θ-リンク（宇宙と宇宙をつなぐリンク）を跨ぎ、定理3.11の「多重ラジアル・アルゴリズム」、対数クンマー対応、正則包（holomorphic hull）といった長大な迂回路を経て、別の宇宙から運んできたデータの対数体積として -|log(q)| を読み取る方法。
望月教授は、この二つが「トートロジー的に（同義反復的に）等価な、二通りの計算方法である」と述べている（報告書は原論文の該当箇所を引用している）。
ここの評価が微妙なところである。「トートロジー的に等価」──これは前回、ショルツェ教授らが「トートロジー（同義反復）に陥っている」と批判したのと、言葉の上ではほとんど同じ表現である。
望月教授にとっては「同じ値を計算する二つの正当な道がある」ことの証しであり、批判者にとっては「何も証明していないのと同じ空回り」の徴候である。同じ現象を、正反対の方向から見ている。
望月教授はどう説明しているか──IPL・SHE・APT
では、別の宇宙から変換されてきた計算結果を、元の宇宙の実数と「同一視してよい」根拠を、望月教授はどう説明しているのか。
報告書によれば、望月教授は多重ラジアル・アルゴリズムが持つ三つの性質を挙げている。専門用語なので、私なりのかみ砕き方で並べておく。
(IPL) 入力素ストリップ・リンク──アルゴリズムの途中で現れる中間的なデータが、完全多重同型（full poly-isomorphism）を介して、入力側のq-パイロットのデータに「結び付いている」という性質。
(SHE) 同時正則表現可能性──出力データやその構築が、Θ-リンクの両側（域側の宇宙と余域側の宇宙）の双方の正則構造において同時に「妥当かつ実行可能で、適切に定義される」言葉で表現できる、という性質。
(APT) アルゴリズム的平行移動──宇宙間の移動が、単に集合を右から左へ動かすような「集合論的な移動」ではなく、共通のコアデータに対して同時に実行できるアルゴリズムとして正当化される、という性質。
そして、この三性質があるからこそ、不確定性（後述するInd1・Ind2・Ind3の「ぼやけ(blurring)」）を伴って構築された出力領域の対数体積の集合は、直接計算されたq-パイロットの対数体積を「可能な値の一つ」として含む。だから最終的に系3.12の不等式 -|log(q)| ≦-|log(Θ)| が導かれる──というのが、望月教授の論法だと報告書は整理している。
ここで大事なのは、望月教授の戦略では、Θ-リンクを跨いで両側の数値を直接比べているのではない、という点である。二つの計算結果は、あくまで「同じ側（右側）の同じ体積コンテナ」の内部で出会い、比較される。Θ-リンクの役割は、両側の数値を直接見比べるための橋ではない。
ショルツェ＝スティックスは、両側の数値を直接見比べており、いわば簡略化したことによって望月教授の証明戦略、主張と、フローが変わってしまっているものを措定して、批判している。これは、ショルツェ＝スティックスの批判を理解するうえで決定的に重要な区別だ、と報告書は強調している。
「壁」の正体──連結亜群と、空虚なリンク
ここからが、AIとの対話を通じて私がいちばん「なるほど」と思った箇所である。
報告書は、望月教授の (IPL)、すなわち「中間データと入力データが同型を介してリンクされている」という主張について、ある意味望月教授にとって手厳しい注記（Remark 8.2.1）を置いている。曰く、「単に二つのデータの間に同型が存在する、というだけの主張は、空虚（vacuous）である」と。
なぜか。報告書が扱うデータ（BPS＝基本素ストリップと呼ばれる簡略化された対象）の集まりは、数学的に「連結亜群（connected groupoid）」という構造をなしている。連結亜群とは、乱暴に言えば「その中の任意の二つの対象の間に、必ず同型（可逆な対応）が存在してしまう」ような世界のことである。実際、報告書の補題（Lemma 4.1.7）は、ある一つの条件（積公式）さえ揃えば、任意の二つのBPSは常に同型になってしまうことを証明している。
だとすると、「出力データと入力データがリンクしている（＝同型が存在する）」と言ってみたところで、それはこの世界では当たり前すぎて何の情報も実質的には伴っていない。「この二つは繋がっている」と言っても、そもそもこの世界では何もかもが繋がっているのだから、証明としては空回りしている。
前回記事で私は、「ローカル変数を他のルーチンの変数と同一視してはいけない、グローバル変数が使えない場面で使ってはいけない」というような、変数（定数）の厳密な使い分けが重要である、IUT理論が変換やカプセル化を繰り返す多くの段階で変数をどうやって混同せず比較可能な変数とみなせるのかが課題、という旨を書いた。その直感はそう外れてはいなかったと思う。
だが報告書が突きつけているのは、変数(定数）の使い分けの問題ともいえるがやや手前の問題であろう。『リンクしている』という述語が、Leanの関数（数学の論理式）として書き下せるだけの中身を持っていない、という指摘である。
報告書は、だからこそ「link」という概念には、Leanで形式化できるだけの、より精密な定義が必要であると述べている。
望月教授が (IPL) で「全ポリ同型でリンクされている」と言うとき、それを額面どおりLeanに翻訳しても、連結亜群ゆえに無内容になってしまう。「繋がっている」の一言で済ませられていた部分を、機械が検証できる形にまで解きほぐさなければならない。ここに、Leanによる形式化ならではの厳しさがある。
数式で言えば──ηの一致 (9-1)
報告書は、この「壁」を一本の数式にまで煮詰めている。2026年2月のサンディエゴ・ブートキャンプで抽出されたという、その核心はこうだ。
二つの同型写像がある。
η^q──q-パイロットと、その宇宙に本来備わった正則構造から、直接得られる同型。
η^anab_S──弱められたデータから出発し、遠アーベル幾何学とクンマー理論で作用を再構築し、対数殻（ログシェル）というコンテナの中で、不確定性を伴いながら「適切な整構造 S」を選ぶことで得られる同型。
証明が成立するために示すべきなのは、適切な S を選べば η^q = η^anab_S となること、これだけである（報告書ではこれを (9-1) と呼んでいる）。
これに対する報告書の評価が、じつに慎重で、曰く、「この関係式 (9-1) は、明らかに偽というわけではない（not manifestly false）。しかし、現時点で我々はその証明を持っていない」。
肯定もしない。否定もしない。「偽ではなさそうだが、証明できていない」。これが、2026年7月時点でのLANAプロジェクトの、いつわらざる到達点なのである。
中間報告では、それが証明のギャップか、プロジェクトのメンバーの理解が届いていないのかは、LANAプロジェクトのメンバーでは結論が出ていないという。誠実なコメントだと思う。
仮に現時点で数学的証明としてギャップがあったとしても、数学的述語の補足や補足証明によって、真と証明される可能性が残るからである。
それは、フェルマーの最終定理のワイルズによる証明でも発生した事態であった。
三つの不確定性（Ind1・Ind2・Ind3）と「ぼやけ」
前回、私はショルツェ教授らの批判を、こう理解して書いた。
「3つの不定性によるずれにより2つの宇宙間のずれが拡がりすぎて比較不可能になっている」という指摘である、というものである。
そしてそれに対する望月教授の再反論、すなわち「宇宙際に写像として投影した場合はぼやけているが、そのぼやけの範囲は数学的対象が巨大であろうと解析可能である」という主張には、首肯すべきものがあるように思われる、とも書いた。
この「3つの不定性」「ぼやけ」が、報告書ではInd1・Ind2・Ind3という三つの不確定性として、より精密に扱われている。
私がAIとの対話でとりわけ知りたかったのは、次の点だった。
望月教授の言う「連結亜群であっても、ぼやけの下で対数体積は計測可能だ」という主張は、Leanで形式化できるものなのか。LANAプロジェクトのメンバーの数学者たちはそれをどう見ているのか。
理解した限りでは、中間報告書の答えは「三段構え」になる。
第一に、なぜ連結亜群（＝対象がみな潰れて区別できない世界）なのに、対数体積という数だけは生き残るのか。報告書の読みでは、情報を担っているのは「対象」そのものではなく、対象から測り取られる実数値の不変量、すなわち対数体積である。
対象のレベルでは何もかもが同型で潰れていても、ハール測度による対数体積という「より粗い物差し」に落とすと、剛化されたq-パイロットが出力領域の中に「一つの可能な値」として姿を現す。
望月教授の言う「ぼやけても数は生き残る」とは、対象が区別できるからではなく、不確定性の軌道が有界に制御され、体積の値が計算可能な集合の中に収まるからだ、という理解である。
第二に、その「ぼやけを支える機構」の周辺部分については、Leanで書く道具立てが、実は見えている。
報告書のRemark 3.3.2は、群を「その解釈（作用）を忘れて、抽象的な位相群として扱う」という操作を、Leanの型クラス（typeclass）でどう実装するかを具体的に論じている。
ある対象に「群としての構造」だけを与え、「作用付きの群としての構造」はあえて与えない──こうすれば、機械は同じ対象を「群としては見るが、作用付きの群としては見ない」。
これはまさに、IUT理論が要求する「素性（provenance）を忘れる」操作そのものであり、「ぼやけ」を成立させる根っこの動作である。ここは形式化の見通しが立っている。
第三に、しかし決定的な一段は、まだ形式的な証明として存在しない。
プロジェクトはこの論争の焦点を絞り込んで、「図式が可換か、ある同型が実質的に恒等写像（id-ness）と言えるか」という、Leanに書ける命題にまで翻訳することには成功した。それ自体が2025年の大きな成果だと報告書は言う。
サンディエゴでの合宿以降、Adam Topaz氏が問題箇所に至る論理の「骨格（skeleton）」をLeanコードとして書き、望月教授の側もそれを土台に「低解像度のLeanコード」で穴埋めを試みた。
両者がLeanコードという共通言語を通じて対話を始めた──ここは、私が前回期待した「デバッグの過程で証明が補完されていく」プロセスが、現に動き始めていることを示している。
だが、そこで得られたものはなお多くの「ブラックボックス」を含み、完全な形式的証明ではない。
しかも今回の中間報告では、Leanコードそのものは公開しないと決められた。そして核心の (9-1) η^q = η^anab_S については、LANAは証明を持たないと明言している。
一言でまとめれば、こういうことになる。
「証明として完成しているなら形式化できるはずだ、そして形式化こそが決着の手段だ」というのがLANAの作業仮説であり、同時に「その形式化の最後の一段は、まだ書けていない」というのが、この報告時点での率直な現状報告なのである。
私が前回書いた「証明の補完がなされてIUT理論は真と証明されるのかもしれない」という見通しは、否定こそされていないが、その「補完」の一段がいかに険しいかが、はっきり可視化されたように思われる。
ショルツェ＝スティックスとの関係──同じ場所を指しているのか
報告書は最終章で、2018年のショルツェ＝スティックス報告書との関係も丁寧に論じている。ここも前回の記事の続きとして、重要な補足になる。
前回、私はショルツェ教授の「同一視できないものを同一視している」という批判に対し、望月教授の「構造のぼやけは解析可能だ」という再反論には首肯すべきものがある、と書いた。
一方で、グロタンディーク宇宙における巨大な素数の集まりが「ぼやけるならランダムな寄せ集めでしかない」という数学的感覚が、ショルツェ教授らの批判の根底にあるようにも思われる、とも書いた。
報告書のスタンスは、ショルツェ＝スティックス、望月どちらか一方に軍配を上げるものではない。
整理するとこうなる。
ショルツェ＝スティックスが提示した（LANA中間報告における）「六角形の図式」が非可換であること、そしてそれを修復しようとすればABC予想を証明するには大きすぎる誤差が生じること自体は、LANAも同意する。望月教授自身も、これは「単一の正則構造・環論の中だけで作業すれば、いつでも起きることだ」と応答している。
しかし──と報告書は続ける──LANA自身の分析では、この六角形の図式は現れない。系3.12の不等式は、Θ-リンクを跨いだ両側の体積を直接比べて得られるのではなく、片側の宇宙の内部で、数論的直線束の次数を比較して得られる。だから、六角形の図式が非可換であること自体は、それだけでは望月教授の意図した証明戦略の破綻を意味しない。
つまり、ショルツェ教授らと望月教授は、同じ場所（実数直線Rの複数のコピーの同一視）を指さしてはいるが、そもそも比較しようとしている図式が違う、というのがLANAの見立てである。ショルツェ教授らが「これは非可換だから救えない」と断じた図式は、望月教授の本来の証明戦略とは別物であるということである。
私の前回の記事で、ショルツェ＝スティックスの批判は簡略化したモデルを前提にして批判しているのでIUT理論の主張と噛み合っていないと指摘していたが、LANAプロジェクト中間報告の見解も同じであった。
そして肝心の点、LANAはショルツェ教授らのように「小さな修正では救えないほど深刻だ」とは断定していない。
修復の可能性についても困難さについても、一切の主張をせず、判断を保留している。
ただし、報告書は正直にこうも書き添えている。
ABC予想の証明が存在するか否かについて、多くのLANAメンバーは「原論文には、少なくとも形式化可能な形での証明は含まれていない」という見解を持っている。しかし、プロジェクトとして完全な合意には至らなかった、と。
「形式化可能な形での証明は含まれていない」──これは「証明が間違っている」とは違う。
「証明はあるのかもしれないが、少なくとも今のLeanと今のメンバーの理解では、機械が検証できる形には書き下せていない」という、抑制的で慎重な言い回しである。
ここには、望月教授が繰り返し訴えてきた「批判者は理論の論理構造を掴み損ねている」という主張と、批判者側の「そもそも検証可能な形になっていない」という主張とが、なお解けないまま残っているということである。
LANAプロジェクト中間報告の「保留」をどう受け止めるか
今回、報告書の原文を読み、AIと対話して、前回記事での楽観は慎重なものに変わった。
この中間報告のいちばんの価値は、結論そのものよりも「何が分かっていて、何が分かっていないのかを、これ以上ないほど正確に言語化した」という点にあると思う。
加藤文元教授はコメントで、「IUT理論の正否について結論を急ぐのではなく、何が理解でき、何がなお理解できていないのかを、できるだけ率直かつ正確に言語化することを重視してきた」と述べている。
裁判でも、争点整理は、その段階で勝負の半ば以上を決めることがしばしばである。
「この事件で本当に争われているのは、この点だ」と両当事者が合意できたとき、初めて審理は前に進む。
長年、望月教授と批判者の間で噛み合わなかった論争が、「(9-1) という一本の等式が証明できるか」「その等式をLeanに書き下せるか」という、誰もが同じ地点を見つめられる形にまで絞り込まれた。これは大きな前進だと思う。
もちろん、絞り込まれた一点が、いちばんの難所であることも判明した。
「繋がっている」という数学的述語が、型理論にもとづく証明支援系のプログラミング言語＝Leanの前では、数学的論理式としてどう書き表されるか、Leanの論理式として100％までの完全な証明責任を負う。
前回、私は「変数の同一視の使い分け」の問題だと書いたが、より正確には「無数にある同一視のうち、どれが正しい一つなのかを、どう決定し、数学的述語として記述できるか」の問題になっているようである。
Leanは、コンパイルの際、数学的論理式として成り立たない記述をエラーとして跳ねてしまう。Leanのこの特性は、プログラミング言語でいえば、C言語に対するRustのコンパイル時のエラーチェック機能を思い浮かべるとわかりやすい。
Ｃ言語がコンパイルの際に跳ねないようなメモリ安全性やマルチスレッドにおけるコードミスであっても、Cの改良言語であるRustではコンパイルの際にエラーとして跳ねることで、コンパイル後の実行ファイルの実行時の致命的エラーを著しく低減してくれる。
そのLeanは型理論にもとづく証明支援系であり、ほぼあらゆる数学の証明がLeanによって形式化できるといわれている。
しかし、IUT理論の数学的述語がLeanの型理論と果たして相性がよいのか、IUT理論が異なる宇宙を、情報を変換し、結びつけ、比較する際に出力される、ぼやけた写像を、異なる宇宙の定数（変数）としてどう区別するのか、また変換過程を関数としてどう表現するのか、果たして変数の出力結果としての定数（実数）が、異なる宇宙の関数からの出力結果と比較できるのか、という点について、私は前回の記事では、望月教授のブログも引用しながら、Leanによる形式化が実現可能かが興味深い、といいながら、含意としては、若干の疑問を示していたが、今回のLANAプロジェクトのメンバーらは、どうやらまさにそこに行き当たっているように思われる。
LANAプロジェクトは、そもそも「Lean for ANAbelian geometry（遠アーベル幾何学）」というのがプロジェクトの名称であり、遠アーベル幾何学にもLeanが適用可能であることを前提としている。そして、その遠アーベル幾何学の延長上にあるIUT理論にも、LeanとMathlibによる型理論により、変数の使い分け、数学的論理式による記述と、コンパイルエラーチェックにより、検証は可能だと考えて取り組んでいると思われる。
私は、前回書いた見通し、つまり、数学的述語の補足と補足証明を積み重ねることで、IUT理論によるABC予想の証明は、いずれ「真」と決着するだろう、ただ、それが「かなりの時間を要する」という前回の但し書きは、想像していたよりもずっと重い意味を持っていた。Leanによる形式化の壁は、思ったより高い。
LANA中間報告書は、単なる「同型」が存在すること（連結亜群であること）はLeanで証明できても、それが「実質的に恒等写像である」とまで言えるのか、その論理的なギャップを現時点では埋められていない（証明を持っていない）と述べている。
かけ算と割り算の繋がりの最後の部分が、連結亜群でしかない、これはLeanによる形式化作業ではより厳密な関係性を記述しないと、証明となっていない、という評価は、望月教授には厳しいものである。
IUT理論の異なる宇宙間を繋いだ結果としてのぼやけた写像が、恒等写像にはなりようがないと思われるので、「実質的に恒等写像である」というLANA中間報告書の記載に落ち着いたのかもしれないが、あくまでLeanにおける型一致を要求されれば、IUT理論は形式化の戦略としてはどん詰まりに突き当たっているのかもしれない。
それでも尚、望月教授の証明戦略のIPL・SHE・APTにより、対数体積は一定範囲に収まるのか。そこもLeanによる形式化は、結論が出ていない。
そして、望月教授は、この点について、さらなる何らかのLeanによる形式化作業が可能な数学的述語の補足や、補足証明を提出することができるのか。
望月教授とLANAが、Leanコードという共通言語で対話を始めたこと、これが、この長い長い論争において、初めて「同じ土俵」が用意されたことを意味するのだとしたら、私はやはり、この壮大なドラマの続きを、引き続き見守っていきたいと思う。
＊本稿は、LANAプロジェクトの中間報告書（Project LANA Interim Report on IUT Theory、2026年7月16日）およびZMCのプレスリリースを、ClaudeおよびGemini Notebookとの対話を通じて読み解いたものです。数学的な内容の理解・表現に不正確な部分、誤りがあることはご容赦ください。