可逆圧縮のはずが、展開できなかった。87年目に崩れた「ヤコビアン予想」をエンジニア目線で整理する

数学界のW杯も同時開催だったんですね

안녕하신게라！パナソニック コネクト株式会社クラウドソリューション部の加賀です。

2026年7月19日、W杯決勝戦が延長にもつれ込んでいた裏側で、数学の未解決問題にも決勝ゴールが決まりました。AI関連のニュースが次々に流れる中で埋もれた感があるので、「何が起きたの？」「それで何が変わるの？」「AIはどこまでやったの？」の3つを、エンジニア目線で整理しておきます。
私は代数幾何の専門家ではないので、証明の細部は後述する先行記事に丸ごと譲ります。

なぜ数学の話題を持ってきたのかというと、私たちの現場でよく見かける壊れ方と同じ構図だったからです。局所的にはどこも正しいのに、全体としては壊れていた。分散システムでもキャッシュ設計でも権限設計でも毎回踏んでいる罠が、87年ぶんのスケールで出てきた話でした。

要点を先に書くと、

• 1939年から87年間だれも真偽を決められなかった「ヤコビアン予想」が、3次元以上で偽と確定した
• 決め手は、Xのツイート1本に収まる¹多項式3本の組。誰のPCでも数秒で検証できる
• 周辺の数学予想が連鎖的に倒れ、ヤコビアン予想とヘッシアン予想に絞れば未解決は2件だけに。バーンダウンチャートが崖を描いた
• AIモデルがクレジットされているが、発見過程は未公開。評価は論文待ち

数学界の決勝ゴール

2026年7月19日、数学者レヴェント・アルポゲ（Levent Alpöge）氏²がXにシュート。

hello there the jacobian conjecture is false thanx to my close friend akhil for asking about it and my other close friend fable for working during the world cup final

((1+xy)^3 z + y^2 (1+xy) (4+3xy), y + 3 x (1+xy)^2 z + 3 x y^2 (4+3xy), 2 x - 3 x^2 y - x^3 z): \C^3\to \C^3,…

— levent (@__alpoge__) July 20, 2026

意訳すると「ヤコビアン予想は偽です。訊いてくれた友人 akhil と、W杯決勝戦の裏で働いてくれたもう一人の友人 fable に感謝」という挨拶と、3変数の多項式が3つ。それだけです。87年ぶんの人類の総力に対して、ツイート1本¹。

そのW杯決勝戦で、合計22本ものシュートが放たれていますが、延長後半フェラン・トーレスのシュート1本が雌雄を分けました。
ちょうど同じ時間帯に、名だたる数学者が87年間に渡って何百本と撃ち込んでも割れなかったゴールを、レヴェント・アルポゲ氏のツイート1本が割りました。
あまりにも出来すぎていて、ちょっと笑いました。（ツイートまでの約4時間は、87年という試合時間から見れば僅かなアディショナルタイム扱いで良いでしょう）

可逆圧縮のはずが、展開できなかった

ヤコビアン予想の中身は、可逆圧縮のエンコーダ／デコーダに置き換えると素直に読めます。

n個の入力を受け取ってn個の出力を返す関数を書きます。使えるのは足し算・引き算・掛け算だけ。割り算も指数も平方根も禁止、要するに多項式だけで書かれたエンコーダです。

このエンコーダには「ヤコビ行列式」という伸縮メータが付いています。各点のまわりで空間の体積をどれだけ伸ばしたか縮めたかを表す数字で、ここがゼロにならなければ「その点の近所は潰れていない、つまり周辺だけならデコードできる」ことを意味します。逆にゼロになる点があれば、そこで空間が潰れている。ロスがある圧縮です。

ヤコビアン予想の主張は、ここからです。伸縮メータが全域でぴったり同じ非ゼロの定数を指しているなら、デコーダも同じ言語（多項式）で書けるはずだ。どこを見てもロスが発生していないのだから、アーカイブ全体としても元に戻せるだろうし、戻せてほしい。素朴で、いかにも正しそうな話です。1939年にオット＝ハインリヒ・ケラーが定式化して以来、正しい証明も反例も出てきませんでした³。

なぜ87年もかかったのか

難しさの正体は「多項式だけ」という制約のほうにありました。

エンコーダに指数関数のような無限に続く関数まで許してしまえば、伸縮メータが全域でぴったり同じ非ゼロ定数なのに、像で別々の部分が重なってしまう例は作れると、ずっと前から知られていたのです（Jacobian conjecture）。ところが使える命令を足し算・引き算・掛け算だけに絞ると、途端に壊し方が見つからなくなる。多項式はお行儀が良すぎて崩し方が誰にも見つからなかった、というのが87年間の実績でした。

反例はこの3行

ツイートに載っていたのが、この式です。

f1 = (1+xy)^3 * z + y^2 * (1+xy) * (4+3xy)
f2 = y + 3x * (1+xy)^2 * z + 3xy^2 * (4+3xy)
f3 = 2x - 3x^2*y - x^3*z

3変数で、f1 から f3 までの多項式の次数は最大7、展開しても全部で16項。伸縮メータは全域でぴったり -2 を指しています。それなのに、次の3点が同じ1点に落ちます⁴。

入力 (x, y, z)	出力 (f1, f2, f3)
(0, 0, -1/4)	(-1/4, 0, 0)
(1, -3/2, 13/2)	(-1/4, 0, 0)
(-1, 3/2, 13/2)	(-1/4, 0, 0)

同じアーカイブから元の3つのうちどれを復元すべきか決められないので、デコーダは原理的に書けません。可逆圧縮のはずが、非可逆だったわけです。

なぜこの3行が反例になるのか、という理由もすでに整理されています。この写像は平面曲線の接線を順番になぞっていく操作にあたり、接線を全部なぞると古典的な双対性の都合でほとんどの点を何度も踏むことになります（arXiv:2608.00222）。
同じ点を3回踏むから、3つの入力が同じ出力になる。偶然引いた当たりくじではなく、理由のある構造でした。

エンジニアには馴染みのある壊れ方だと思います。ブロック単位のチェックサムは全部合っているのに、アーカイブ全体が復元できない。局所の健全性をいくら積み上げても大域の健全性にはなりません。

なお圧縮の比喩で説明していますが、実際の圧縮技術が変わる話ではありません。有限のビット列なら単射な写像には最悪ルックアップテーブルという逆写像が必ず存在するので、そもそも「逆が存在するか」は問題になりません。ここで問われているのは「逆が多項式という同じ言語で書けるか」という形式の話です。

実際に手を動かして確かめたい方は、kyamaz氏のQiita記事「ヤコビアン予想（n ≥3）が否定的に解決を確かめる」を参照ください。SymPyで伸縮メータと呼んでいるヤコビ行列式 det J(F) が -2 になるところから、証明を機械で検査する Lean 4（Mathlib）で「多項式の逆写像を持たない」ことを定理として通すところまで、検証コードが揃っています。数分で追体験できます。このスピード感はすごい。

ツイート1個で、大山を鳴動させた

この反例1個が、論理的に等価だったり兄弟関係にある数学の予想を巻き込んで、ドミノ倒しを起こし、今もなお続いています。
依存関係の深いライブラリに破壊的変更が入った時のドタバタが、数学界で起きたわけです。

巻き込まれた予想	どうなったか	まだ残っている範囲
ディクスミエ予想 「ワイル代数 A_n の自己準同型は必ず自己同型」	ヤコビアン予想と等価性が証明済みだったため自動的に偽	A_1 と A_2 だけ
ポアソン予想 「2n変数のポアソン代数で同様」	同じく等価だったため同時に偽	2変数と4変数だけ
ヘッシアン予想 （Hessian conjecture）	反例を6変数に倍化して1変数だけ部分ルジャンドル変換し、5変数の反例を構成。5変数以上で偽	4変数だけ
弱マーカス＝ヤマベ予想	反例から14次元上にベクトル場を構成。14次元以上で破綻	3〜13次元

「局所的にどこも潰れていないなら、大域でも1対1のはずだ」という素朴な期待が、まとめて崩された格好です。等価性が証明されている予想は、片方を直せば片方も直るという便利さの裏返しで、片方が倒れると自分も倒れてしまいます。

面白いのは、87年ぶんの研究が無駄になっていない点です。人類はこの間、「多項式の次数が2以下なら真」「双有理なら真」といった肯定的な部分結果を積み上げてきました。通ったテストケースの山です。反例が出た今、既存のテストケースは全部グリーンだけど、テストがカバーできていない領域にバグがいたと判明したわけです。そりゃドタバタになります。

ただ、明日の業務に効く応用があるかというと、ありません。書き換わったのは代数幾何と可換環論の基礎命題群のほうです。それでも、既視感のある構図だったので、エンジニアだからこそ共有できると思ったのです。

【コラム】「次数100まで調べ尽くしたのでは？」への回答
この件で「人類はコンピュータで次数100まで全探索していたのに」という話をよく見かけますが、あれは2次元の話です。ツォン＝ツェン・モーが1983年に2次元版を次数100以下で検証し、2025年にトゥイ・グエンが104まで押し上げています。無限遠での振る舞いを絞り込んだ結果も、反例の形を制限してきた一連の結果も、やはり2次元です。

では3次元ではどこまで潰せていたのか。多項式の次数2までは証明済みだったので、「反例があるなら次数3以上」までです。今回、次数7に反例が座っていたのを見つけた。
ロンドン大学クイーン・メアリー校のアビシェーク・サハ氏も、直感的に正しそうに聞こえるので、反証しようとした人はそれほど多くなかったと思う（有料記事）、という趣旨のことを述べています。灯台下暗しというより、灯台は87年間フル稼働していたのに、光が向いていたのはほとんど2次元のほうだったという話です。

AIの関与は、論文待ち

ニュースとしては「AIが87年来の難問を崩した」が見出しになりました。サハ氏は他のAI絡みの成果と比べたうえで、これまでにAIが重要な役割を果たした中で最大の予想だろう、という趣旨の評価をしています。

「最大」が何との比較なのかは、2026年のニュースの並びを見ると分かります。5月にOpenAIの非公開モデルがエルデシュの単位距離予想（1946年）に反例を出し、エルデシュが残した問題群が次々とAIに崩されているという流れができました。7月にはディニッツ＝ガーグ＝ゲーマンス予想の反例がXに投稿され、8月にはOpenAIが長年の未解決問題を10問まとめて解いたと発表しています。つまり「AIが予想を崩す」こと自体はもう珍しくない。その中でヤコビアン予想が最大とされたのは、87年という長さと、スメールが次の世紀の宿題に選んだ18問に入っていたからだと推測します。New Scientistは見出しでAIが解いた中で最も難しい問題だと専門家は言うとまで書きました（有料記事）。

ただ、そこを評価するには材料が足りません。
アルポゲ氏がツイートで感謝した「もう一人の友人 fable」は、AIモデル「Claude Fable 5」でした。ただしプロンプトも会話ログも公開されておらず、査読を通った論文も出ていません（本当に友人の名前だったらどうしよう）。そのサハ氏も、反例の検証自体は簡単だが、どうやってそこに辿り着いたのかは不明だ、という趣旨のコメントをしています。人間とAIとツールがどこで何をどこまで分担したのかは、いまも分からないままです。

それでも、輪郭くらいは見えています。
まず、素朴な総当たりで届く規模ではありません。3変数7次までの単項式は120種類あり、そこに整数係数を割り振って3成分ぶん決める組み合わせは天文学的です。テレンス・タオもこの反例の解説で、伸縮メータを定数に保つという条件が使える自由度をはるかに超える本数の等式になるので、総当たりで見つかる見込みは薄いという趣旨の評価をしています。モナシュ大学のメリッサ・リー氏も、今回の難しさは込み入った構成や長い証明ではなく、膨大な探索空間をうまく歩く方法を見つけるところにあったようだ、という趣旨の整理をしています。証明を組み立てるAIではなく、物を探し当てるAIだった、というのが今回の性格でした。組み合わせを探し当てると言うと量子コンピュータを連想しますがどうやら違っていそうです。もし量子でゴリ押したなら、クレジットされる名前は fable ではなかったでしょう。
そして出てきた反例は正しい。検証可能で、疑う余地がありません。

この「論文を待つ」という態度、私個人の慎重さというわけでもありません。
反例の1か月半前、2026年6月2日に公開されたライデン宣言が、AIを使ったなら開示すること、正しさと引用の責任は人間が最後まで持つこと、査読のある場で公表することを求めていて、国際数学連合（IMU）も支持を表明しています⁵。
今回の件は、このうち査読の層だけがまだ乗っていない状態です。

発表から1か月以上が経ちますが、発見過程を書いたものは本人から出てきていません。周辺はこの間ずっと全力疾走で、形式検証は当日、関連するプレプリントは翌日から出始め5週間で10本近く、幾何的な言い換えも一般向けの解説サイトも出揃いました。
この速さの中で、中心にある「どうやって見つけたのか」だけがぽっかり空いたままです。壁が崩れる音は誰でも数秒で確認できるのに、崩し方の説明だけがまだ届いていない。

というわけで、AIの寄与がどれほどのものだったかは論文が出るまで保留です。

線引きは、賢さではなく検証コストで

私が面白いと思って記事にしたかったのは、この件が「探索は絶望的に難しいが、検証は数秒で終わる」構造だった点です。ハッシュの逆算、RSAの柱となる素因数分解、PoWのノンス探索と同じ、エンジニアにはお馴染みの非対称性です。

ここは自分の仕事に持ち帰れる話だと思っています。検証が安い問題なら、探索はAIに投げてよい。出てきた答えの正しさを機械的に判定できるなら、どうやって思いついたのかが不明でも使えます。逆に検証コストが高い問題、たとえば「この設計が5年後も保守できるか」みたいな問いでは同じ戦法が効きません。AIに何を任せるかの線引きは、賢さではなく検証コストで分けるほうが実用的です。

【コラム】証明のCIが回った日
発表当日にLean版の検証リポジトリが立ち、そのあと証明を機械が1行ずつ検査するツール「Isabelle」でも独立に形式検証され、Archive of Formal Proofs にエントリが登録されました⁶。伸縮率が恒等的に -2 であること、異なる3有理点が同じ像を持つこと、多項式の逆写像を持たないことが、機械検査済みの定理として並んでいます。
このエントリのライセンス欄には、証明の組み立てにAIの支援を使ったこと、そして最終的な定義と定理と証明はツール側が検査していることが明記されています。AIが書き、機械が検査し、人間が責任を持って公開する。私たちが普段やっているコードレビューやCIと、驚くほど同じ形です。発見プロセスが不明でも結果を信用できるのは、この検証の層が効いているからです。
ちなみに同じ7月、ディニッツ＝ガーグ＝ゲーマンス予想の反例も同じくAFPに登録されています。ライセンス欄の文言はヤコビアンのエントリと一字一句同じ。この作法がもう定型になりつつある、ということだと思います。

最後に残った2次元が決まると、どうなるのか

3次元以上が偽と決まったので、ヤコビアン予想とヘッシアン予想の2族に絞れば、未解決なのは「2次元のヤコビアン予想」と「4変数のヘッシアン予想」の2つだけになりました。しかもこの2つは「4変数のヘッシアン予想が真なら2次元のヤコビアン予想も真」という依存関係まで整理されています。87年かかっても輪郭がハッキリしなかった問題が、一気に残タスク2件になったわけです。バーンダウンチャート崖過ぎぃ！

1884年のクラウス以来142年。2次元の真偽がどちらに転んでも、スティーヴン・スメールが1998年に挙げた18問の「次の世紀の数学問題」の16番チケットは閉じます。
違ってくるのは、閉じ方です。

2次元も偽だった場合、その反例は少なくとも次数105以上になります。次数104までは真だと検証済みなので、それより上にしか居場所がありません。3次元では次数7だったためツイートに収まりました¹が、次に出てくるものはエグいサイズになる。つまり「人間が見て納得できる反例」の時代が終わり、反例が人間可読性を失う最初のケースになり得ます。検証は機械がやってくれるとしても、なぜそれで反例になっているのか人間の側がまるで腹落ちしない、という状況が起き得ます。

2次元が真だった場合、宿題が1問増えます。「なぜ3次元以上では壊れるのに、2次元だけは安全なのか」を説明しないといけない。ヒントらしきものは2つ転がっていて、ひとつは平面の可逆な多項式変換が必ず決まった基本操作の列に分解できると証明済みなこと（1942年のユンクの定理）、もうひとつは今回の反例が無限遠へ逃げていく経路を通してのみ復元不能になることです。3次元にはどちらの縛りも知られていません。

ヒントの1つ目はエンジニアには見覚えのある形をしています。分解先の基本操作のひとつが「y はそのまま通して、x のほうに y の関数値を足す」で、DES暗号とかで使われているFeistel構造の1ラウンド（スワップなし）と同じなのです。片側を触らずに相手の関数値を混ぜるので、中の関数が何であっても必ず元に戻せる。平面ではどんな可逆変換もこのラウンドの積み重ねに必ずコンパイルできると分かっていて、3次元にはそのバイトコードに落ちない変換が実在します⁷。反例が3次元で出たのは、その意味で筋が通っています。

ヒントの2つ目は境界の外側にだけ潜んでいたバグです。有限の範囲に収まっているあいだはどの点も健全で、テストは全部グリーン。壊れるのは値が範囲の外へ抜けていく経路を通ったときだけで、オーバーフローや範囲外アクセスと同じ形です。平面はこの抜け道が狭いことが古くから知られていますが、3次元では抜け道が何本あるのかも分かっていません。境界の外を全部確かめろと言われているのに、境界がいくつあるか誰も知らない状態です。

そして「なぜ次元が上がると壊れやすくなるのか」自体が、まだ誰にも説明できていません。そこが分からないからこそ、2次元の決着とその後の研究に期待が高まります。

まとめ

技術的な要点はこれです。ブロック単位で全部正しいことは、全体が正しいことを保証しない。
伸縮メータが全域で一定だろうと、アーカイブが展開できる保証にはならなかった。しかも87年間、既存のテストは全部グリーンでした。分散システムでもキャッシュ設計でも権限設計でも、私たちが何度も踏んでいる罠とまったく同じ形です。今回は踏んだ業界が違っただけなんやな、と。

AIについて分からないのは、過程だけです。役割分担はハッキリしていて、探索はAIが担い、問題の選定と検証と公開の責任は人間に残りました。問題を持ちかけたのはマシュー氏、検算したのは世界中の数学者と証明検査ツール、名前を出して公開したのはアルポゲ氏です。AIも、証明を組み立てるAIではなく物を探し当てるAIでした。出てきてないのは「どうやって探し当てたのか」だけ。

持ち帰れるのは、線引きの基準です。AIに何を任せるかは、賢さではなく検証コストで決まる。答えの正しさを機械で判定できるなら、AIの思いつき方が不明でも使えます。逆に「この設計が5年後も保守できるか」みたく検証コストが掛かる問題は、どれだけ賢いモデルが出たとしても任せられません。

エンジニア目線で驚いたのは、検証容易性です。87年間守られていた壁が、ツイート1本のサイズで、しかも誰の手元でも数秒で確認できる形で崩れました。また、公開後に関連するプレプリントが5週間で10本近く出たスピード感も、研究者間が手紙で往復していた時代からは隔世の感があります。

数式の中身と検証コードを追いたい方は、あらためてkyamaz氏のQiita記事へどうぞ。SymPyで数行叩くだけで、あの壁が崩れる瞬間を自分の手で再現できます。なかなか贅沢な体験でした。

---

お断り
記事内容は個人の見解であり、所属組織の立場や戦略・意見を代表するものではありません。
あくまでエンジニアとしての経験や考えを発信していますので、ご了承ください。

本記事の数学的事実は、英語版Wikipedia「Jacobian conjecture」を入口に、本文中にリンクした各原論文・arXivプレプリント・Archive of Formal Proofs のエントリ・各報道で裏を取っています。反例の発見プロセス（プロンプトや会話ログ）は公開されておらず、査読論文も出ていないため、AIの関与に関する記述は本人の公開言及と報道の範囲に留めています。

1. New Scientist（2026年7月20日付、有料記事）はこの反例を「216文字」と紹介しています。140文字時代なら入らなかったサイズです。2017年に上限が280文字になったのは、たぶんこの日のためでした。 ↩ ↩² ↩³

2. 報道と英語版Wikipediaでは、アルポゲ氏はハーバード大学の数学者であり、かつAnthropic所属と紹介されています。ツイート中の「akhil」はシカゴ大学のアキル・マシュー（Akhil Mathew）氏で、この問題を持ちかけた人です。発表は米国東部時間の7月19日で、W杯決勝戦も同じ日でした。ただし協定世界時（UTC）では日付をまたいで7月20日になるため、埋め込んだツイートやWikipediaの出典表記は「July 20, 2026」になっています。 ↩

3. 2変数版はさらに古く、1884年にルートヴィヒ・クラウスが（誤った証明付きで）述べていたことが、2025年のzbMATH調査で判明しています（On the origin of the Jacobian conjecture）。この問題は最初の一歩から「解けた気になって公開したら間違っていた」で始まっているわけです。その後も誤った証明が繰り返し出ていて、ベニアミーノ・セグレやヴォルフガング・グレブナーといった大物も外していると紹介されています。このグレブナー氏、多項式の連立を機械で解くときに使う「グレブナー基底」の名前の由来になった人です。そのグレブナー基底が、今回は反例のファイバー構造を確かめる計算に回っています。証明を間違えた本人の名前が付いた道具で、その予想が崩れたことを検算している格好です。 ↩

4. 反例として必要なのは、同じ点に落ちる入力が2つあることだけです。3つ並んでいるのは気前がよかったからではなく、この写像の素の姿がそうだから。逆算の式が3次方程式に落ちるので、ほとんどの出力はもともと3つの入力から来ています（The Jacobian counterexample, explained）。2つで済ませる自由は、最初から無かったわけです。 ↩

5. 2025年9月にライデン大学ローレンツセンターで開かれた会議「Mechanization and Mathematical Research」（10か国から約60名）を起点に、以降8か月かけて16名のワーキンググループがまとめたものです。数学者が中心ですが、哲学者・計算機科学者・数学史研究者も入っています。署名は本記事執筆時点で3600名超。IMU以外にも、ピーター・ショルツェ、テレンス・タオ、ケヴィン・バザードといった面々が個別に賛同を寄せています。宣言では技術企業との連携や誇大宣伝についても踏み込んでいます。今回の件と重ねて読むと考えるところがあるので、別稿で扱う予定です。 ↩

6. 正式には Isabelle/HOL と書きます。Isabelle が定理証明支援系の名前、HOL は高階論理（Higher-Order Logic）の略で、その上で使う論理体系を指します。kyamaz氏の記事に出てくる Lean 4 も同じ種類のツールで、証明を型検査のように機械で通す仕組みです。人名ではありません（どうぶつの森のしずえさんの英語名も Isabelle なので筆者は混乱しました）。 ↩

7. この「分解の仕方を知らないと逆算できない」性質をトラップドアに使ったのが、多変数公開鍵暗号のTTM（Tame Transformation Method）です。提案者は次数100の検証をやったモー本人でした。平面だと分解アルゴリズムが存在してしまうので鍵になりません。ただしTTM自体も2000年のGoubin＝Courtois攻撃以降、複数の解読報告が出ています。難しさを鍵にするのは、やっぱり難しい。 ↩