はじめに
2026年7月20日、Anthropic の研究者である Levent Alpöge 氏が、Claude Fable 5 を使ってヤコビアン予想の反例を得たと報告しました。ヤコビアン予想は、代数幾何の分野で長年未解決とされてきた問題です。
この種のニュースは「AI が◯◯年来の難問を解いた」という形で流れがちですが、数学の反例は、生成された時点では何も確定していません。 確定するのは、第三者が検証したあとです。
そして今回の件は、その検証がどこまで進んでいるかが極めて特徴的でした。
- 報告されたのは 3変数の多項式写像。ヤコビ行列式は定数1なのに、異なる2点が同じ像に写る。筆者も手元で厳密に確認した
- Lean による形式化が提出され、リポジトリの CI ビルドを通過している。 これは「SNS の主張」よりはるかに強い状態
- ただし 査読論文もプレプリントも存在せず、PR はまだマージされていない。2変数の場合は未解決のまま。 そして「なぜこの例が効くのか」の人間による理解はこれから
1. 🧩 ヤコビアン予想とは何か
ヤコビアン予想は、「多項式で作った変換」についての問題です。
ここでいう変換とは、平面上の点を、多項式で計算した別の点へ移す操作のことです。たとえば次のものがそうです。
(x,\ y) \ \longmapsto \ (\,x + y,\ \ y\,)日本語で読み下すと「x 座標には y を足す。y 座標はそのまま」という操作です。点 (2, 3) なら (5, 3) へ移ります。平面全体で見ると、上にある点ほど右へずれるので、四角形が平行四辺形にひしゃげるような変形になります。
こうした変換について、知りたいことが2つあります。
- 戻せるか — 移った先の点から、元の点へ逆にたどれるか
- 戻し方も多項式で書けるか — 逆にたどれるとして、その戻す操作もまた多項式で書けるか
上の例は、どちらも「はい」です。戻す操作は次のもので、
(u,\ v) \ \longmapsto \ (\,u - v,\ \ v\,)「u から v を引く。v はそのまま」という、やはり多項式だけで書けた操作です。実際 (5, 3) を入れると (2, 3) に戻ります。
「戻せる」と「戻し方が多項式で書ける」は別の話
2番目の問い(戻し方も多項式で書けるか)は、一見すると当たり前に思えます。戻せるなら書けるだろう、と。ですがそうとは限りません。
変数を1つに減らすと、分かりやすい例があります。
x \ \longmapsto \ x^3これは戻せます。結果が 8 なら元は 2、27 なら 3 です。1番目の問いは「はい」。 ところが戻す操作は3乗根であって、多項式では書けません。2番目の問いは「いいえ」です。
つまり「戻せること」と「その戻し方が多項式で書けること」は、別々に問う必要があるのです。ヤコビアン予想が扱っているのは、この2番目のほうです。
見分ける手がかり — ヤコビ行列式
では、どんな変換なら戻し方まで多項式になるのか。 それを見分ける手がかりになるのが、ヤコビ行列式(ヤコビアン) と呼ばれる量です。
作り方は単純で、変換の各成分を各変数で偏微分して並べ、その行列式を取ります。さきほどの (x+y,\ y) で実際にやってみます。
J = \begin{pmatrix} \dfrac{\partial (x+y)}{\partial x} & \dfrac{\partial (x+y)}{\partial y} \\[6pt] \dfrac{\partial y}{\partial x} & \dfrac{\partial y}{\partial y} \end{pmatrix} = \begin{pmatrix} 1 & 1 \\ 0 & 1 \end{pmatrix} , \qquad \det J = 1 \times 1 - 1 \times 0 = 11という定数になりました。 x にも y にも依存しません。
この値には意味があります。ヤコビ行列式は、その点のまわりで空間がどれだけ伸び縮みしているかの倍率を表します。今の例で 1 になったのは、平面をひしゃげさせてはいるが、面積はどこでも変えていないということです。
そして倍率がどこでも同じ値で、しかも0でないなら、空間はどの場所も同じ割合でしか変形しておらず、潰れても折り重なってもいないはずです。潰れていないなら、別々の点が同じ場所へ重なることもなく、逆にたどれるはずです。
では、ヤコビ行列式が0でない定数でありさえすれば、戻し方まで多項式で書けるのでしょうか。 これがヤコビアン予想です。
ここからは、手で計算できる小さな例で確かめていきます。以下に出てくる例は説明のためのもので、今回報告された反例そのものではありません(実際の反例は §2 で扱います)。
まず、1変数だとつまらない
1変数の多項式 f(x) を考え、「微分がどこでも同じ、0でない定数」という条件を課してみます。
f'(x) = c \ (c \neq 0) を満たす多項式は、 f(x) = cx + d しかありません。つまり直線です。 直線なら逆にたどるのは簡単で、 x = (y - d)/c 。これも多項式です。
1変数では、条件を課した時点で答えが出てしまう。 だから問題になりません。
なお冒頭に出した x \mapsto x^3 は、微分が 3x^2 で定数ではないので、そもそもこの条件を満たしていません。 「逆が多項式にならない」例が条件から外れてくれる——この条件が付いている理由が、ここに見えます。
2変数にすると、急に面白くなる
変数を2つに増やします。次の写像を見てください。
F(x, y) = (\,x,\ \ y + x^2\,)「 x はそのまま、 y は x^2 だけずらす」という操作です。平面を放物線状にゆがめる、と思ってください。
各成分を各変数で偏微分して並べると、次の行列になります。これがヤコビ行列です。
J_F = \begin{pmatrix} \dfrac{\partial}{\partial x}(x) & \dfrac{\partial}{\partial y}(x) \\[4pt] \dfrac{\partial}{\partial x}(y + x^2) & \dfrac{\partial}{\partial y}(y + x^2) \end{pmatrix} = \begin{pmatrix} 1 & 0 \\ 2x & 1 \end{pmatrix}行列式は 1 \times 1 - 0 \times 2x = 1 。 x にも y にも依存しない、ただの定数1になります。
では逆にたどれるでしょうか。たどれます。
G(u, v) = (\,u,\ \ v - u^2\,)実際に代入すると G(F(x,y)) = (x,\ (y + x^2) - x^2) = (x, y) で、ちゃんと元に戻ります。逆向きも同様です。そしてこの G も多項式です。
ここが大事なところです。この F は直線ではなく曲がっています。それでも「ヤコビ行列式が0でない定数」という条件を満たし、しかも多項式のまま逆にたどれる。
つまり2変数以上では、1変数のときのように「条件を課したら直線しかない」とはならず、曲がった例がいくらでも作れます。 それでいて、作ってみるとどれも多項式で逆にたどれてしまう。
では、いつでもそうなのか——これが予想
上の例はうまくいきました。他にどんな例を作ってみても、やはりうまくいきます。ならば、いつでもそうなのでしょうか。
これを一般の n 変数で書いたものが、ヤコビアン予想です。
\underbrace{F : k^n \to k^n}_{\text{各成分が多項式}} \ , \quad \underbrace{\det J_F = c \neq 0}_{\text{0でない定数}} \quad \Longrightarrow \quad \underbrace{F^{-1} \ \text{も多項式}}_{\text{多項式のまま逆にたどれる}}言いかえると、こうです。
ヤコビ行列式が「0でない定数」でありさえすれば、その多項式写像は必ず多項式で逆にたどれる。
「必ず」と言えるのか。 それが1939年以来、誰にも証明も反証もできなかった問題です。
ちなみに Google DeepMind の Formal Conjectures リポジトリにある形式化では、この予想は「ヤコビアンが0でない定数であるような正則写像(=多項式で与えられるベクトル値写像)は、多項式で与えられる逆写像を持つ。ただし k は標数0の体」と述べられています。上の説明と同じことを、数学の言葉で言ったものです。
- 正則写像(この文脈では)… 各成分が多項式で書けている写像のこと。上の F(x,y) = (x, y+x^2) がまさにそれです
- 体(たい) … 足し算・引き算・掛け算・割り算が自由にできる数の世界。有理数・実数・複素数はどれも体です
- 標数0 … 1をどれだけ足しても0にならない、という性質。有理数・実数・複素数はすべて標数0です。「普通の数で考える」と読んで差し支えありません
逆に標数が0でない世界(有限体など)では、そもそも古くから反例が知られています。今回の話はそちらではありません(§FAQ の Q2 で改めて触れます)。
なぜ「成り立ちそう」に見えるのか
冒頭で書いた直観をもう一度置きます。ヤコビ行列式が0でない定数ということは、空間がどこでも同じ割合でしか変形していない、つまり潰れても折り重なってもいないということです。 潰れていないなら、別々の点が同じ場所へ重なることはないはずで、だから逆にたどれるはずだ——という感覚です。
上で見た2変数の例も、まさにそのとおりに振る舞いました。この直観が非常にもっともらしいことが、この予想が87年間も残った理由でもあります。
だから、今回の反例は驚きなのです
今回報告された反例は、まさにこの直観を破るものです。ヤコビ行列式はどこでも定数なのに、異なる2つの点が同じ場所へ写ってしまう。つまり「潰れていないはずなのに、重なっている」。
その具体的な形を、次の節で見ます。
補足:この予想は誰がいつ提起したのか
この予想は O. H. Keller 氏が1939年に提起したとされてきました。ただし2025年12月の arXiv 論文「On the origin of the Jacobian conjecture」は、同じ主張が1884年の L. Kraus 氏の論文の主定理として既に現れていると指摘しています(Kraus 氏の証明は最後の段階に欠陥があるとのこと)。
そう考えると、「87年来」という年数の数え方自体に揺れがあることになります。年数を強調した見出しには注意したほうがよさそうです。
2. 🔢 報告された反例そのもの
形式化されたファイルに書かれている多項式写像は、次のものです。3変数( n = 3 )です。
F(X,Y,Z) = \begin{pmatrix} (1+2XY)^3 Z + 4Y^2(1+2XY)(2+3XY) \\ Y + 3X(1+2XY)^2 Z + 12XY^2(2+3XY) \\ -X + 3X^2Y + X^3Z \end{pmatrix}この写像について、形式化では次の2つが証明されています。
- ヤコビ行列式が 定数1 であること(
det_jacobian_F) - 異なる2点
(1, -3/4, 13/4)
と
(-1, 3/4, 13/4)
が同じ像に写ること(
aeval_F_eq)
2 が成り立てば F は単射ではなく、逆写像を持ちません。一方 1 より、ヤコビ行列式は0でない定数です。予想が要求する条件を満たしているのに結論が成り立たない——これが反例と呼ばれている理由です。
筆者による確認
この2点は、こちらでも計算して確かめました。 上の多項式を有理数の厳密演算(浮動小数点を使わない)で扱い、偏微分から 3×3 のヤコビ行列式を展開したところ、次の結果になりました。
| 確認項目 | 結果 |
|---|---|
| ヤコビ行列式 | 定数の 1(他の項がすべて消える) |
| F(1, -3/4, 13/4) | (-1/8,\ 0,\ 0) |
| F(-1, 3/4, 13/4) | (-1/8,\ 0,\ 0) |
| 2点は異なるか | 異なる |
ただしこれは「書かれている主張のとおりになっている」ことの確認であって、予想全体に対する検証ではありません。その意味づけは §4 で扱います。
一部の報道では「ヤコビ行列式は -2」「3つの異なる入力が (-1/4, 0, 0) に写る」と書かれています。上記の形式化とは値が違います。
独立して形式化を行ったリポジトリの説明によると、元の形はヤコビ行列式 -2 の形で、それを 1 にリスケールした形も併せて用意されている、とのことです。標数2の体でも成立させるためにリスケール版が使われています。
つまり同じ反例の別表現である可能性が高く、矛盾しているわけではなさそうです。上で扱っているのは、形式化されたコードに書かれている値のほうです。
3. ✅ どこまで検証されているのか
「SNS で主張された」と「機械が検証した」と「数学界が受け入れた」は、それぞれ別の段階です。
現時点で確認できた検証の状況は次のとおりです。
| 段階 | 状況 |
|---|---|
| 報告 | Levent Alpöge 氏(Anthropic)が X に投稿。Anthropic の組織としての公式発表ではない |
| プレプリント | 見つからなかった(arXiv 上で該当するものを確認できず) |
| Lean 形式化 | Paul Lezeau 氏(Imperial College London)が手作業で形式化し、Google DeepMind の Formal Conjectures リポジトリに PR として提出(2026年7月20日 06:16 UTC) |
| 形式化のビルド | 当該 PR の CI で Build project が pass(所要 1時間39分) |
| レビュー | APPROVED。ただしまだマージされていない(執筆時点で state は OPEN) |
| 独立した形式化 | 別リポジトリ(deancureton/jacobian)に、独立した Lean 4 形式化が存在する |
| 査読 | なし |
| 人間による理解 | これから(後述) |
Lean 形式化が意味すること
Lean は定理証明支援系で、証明のすべてのステップを機械がチェックします。「それっぽく見える議論」は通りません。したがって、形式化されたものがビルドを通っているなら、その主張の論理的な正しさは機械的に保証されています。
これは「AI が出した答えを人間がざっと眺めて納得した」とは全く違う水準です。今回の件が単なる SNS の主張と決定的に違うのはこの点です。
独立形式化リポジトリの説明によれば、そちらの主定理は「任意の体 K 上で K^3 の多項式自己写像であってヤコビ行列式が1、かつ単射でないものが存在する」という形になっており、複素数体への特殊化も別の定理として用意されているとのことです。
それでも「解決した」と書けないこと
Kevin Buzzard 氏(Imperial College London、mathlib メンテナ)は、7月20日のブログで一連の出来事を記録したうえで、「次のステップは、この例で何が起きているのかを人間が正確に理解することだ」と書いています。形式的に検証されていることと、数学として理解されていることは別だという指摘です。
また Buzzard 氏は当該 PR に対して、「予想を解決するこの PR が、同時に予想の主張そのものを書き換えているのは少し驚きだ」とコメントしています。これに対しリポジトリのメンテナは、「否定形を書くために文言の変更が必要になった」「変更点と理由をコミットメッセージで説明したほうがよい」と応答しています。
このやり取りは、反例の数学的な正しさを疑うものではなく、リポジトリの運用に関する指摘と読むのが自然です。ただし「予想の形式化された文言が変更された」という事実は、外から見たときに何が反証されたのかを分かりにくくする要素ではあります。
当該 PR には、独立形式化リポジトリを監査したという報告のコメントが付いています(ビルドが通ること、sorry や独自公理が使われていないこと、#print axioms の出力が標準的な3つの公理のみであることなど)。
ただしそのコメントの冒頭には、「この作業は私の指示のもと Claude(Fable 5)が実施した。以下の文章のほとんども Fable が起草した」と本人が明記しています。
つまりこれは、同じモデルによる自己確認に近い性質を持ちます。有用な情報ではありますが、人間による独立検証として数えることはできません。
4. ⚠️ 「87年来の難問が解決」と書けない理由
まだ「解決した」と言えない理由は、次の5点です。
- 査読もプレプリントも存在しない。 現時点の根拠は、SNS の投稿と GitHub 上のコードです。コードは検証可能ですが、数学界の公式な記録としては、まだ何も提出されていません
- 2変数の場合は未解決のまま。 形式化された PR の中でも、2変数版は「未解決」として明示的に残されています(証明は
sorry、分類も research open のまま)。予想の中でも最も注目されてきた n = 2 の場合は、今回の反例では動きません - 人間の理解がこれから。 §3 のとおり、Buzzard 氏自身が次のステップとして挙げている段階です
- PR がまだマージされていない。 承認は出ていますが、リポジトリに取り込まれた状態ではありません
- この分野は歴史的に、誤った証明・反例の発表が繰り返されてきた。 §1 で触れた1884年の Kraus 氏の論文も、最後の段階に欠陥があったとされています
逆に言えば、「まだ何も信用できない」というのも同じくらい不正確です。Lean 形式化がビルドを通っているという事実は、過去のこの種の騒動とは明確に違います。解決したのでも、眉唾なのでもなく、どちらとも違う段階にあるというのが実際のところです。
5. 🤖 Claude Fable 5 は具体的に何をしたのか
形式化されたコードのコメントでは、この反例は「Alpöge 氏 / Fable の反例」と記されています。つまり Fable 5 の役割は、反例となる多項式写像そのものを生成(探索)したことです。
一方、Formal Conjectures への Lean 形式化は Paul Lezeau 氏が手作業で行っています。 Buzzard 氏のブログにも、Alpöge 氏の投稿の後、Lezeau 氏が手で形式化して PR を出した経緯が書かれています。「AI が証明まで自動で書いた」わけではありません。
ただし Buzzard 氏の同じ記事には、別の問題(有限自由群スキームに関する Grothendieck の問いへの反例)については、Fable が1076行の Lean ファイルへ全体を自動形式化したという記録があります。今回のヤコビアン予想の件とは別の事例ですが、自動形式化まで到達している例が同時期に存在するということです。
整理すると、「AI が難問を解いた」というより「AI が候補を大量に生み出し、人間と機械検証がそれを受け止める」という分業が実際に回り始めている、という話です。エンジニアにとって重要なのは後者の構図だと考えます。生成の速度に対して、検証の側が追いつくかどうかが問題になります。
このモデルについて
主題となっている Claude Fable 5 は、2026年6月9日に公開された直後の6月12日に、米政府の輸出管理指示によって全ユーザー向けに停止され、6月30日の解除を経て7月1日に再展開されたモデルです。その経緯は Claude Fable 5 はなぜ3週間止まったのか|輸出管理指示と再展開を一次情報で整理 にまとめています。
輸出管理で止められたモデルが、再展開の3週間後に数学の未解決問題に触れている——この並びは、いまの AI をめぐる状況をよく表しているように思います。
まとめ
- Anthropic の Levent Alpöge 氏が、Claude Fable 5 でヤコビアン予想の反例を得たと報告した。対象は標数0を含む体上の3変数多項式写像で、ヤコビ行列式は定数、かつ単射でない
- Lean による形式化が Google DeepMind の Formal Conjectures に提出され、CI のビルドを通過。レビューは承認済みだが未マージ。独立した形式化リポジトリも存在する
- 査読論文もプレプリントも無い。2変数の場合は未解決のまま残されている
- Fable 5 がしたのは反例の生成。Formal Conjectures への形式化は人間が手作業で行った
- 「解決した」と言える段階ではないが、「根拠のない主張」でもない。機械検証は通っていて、人間の理解と査読がこれからという、これまであまり無かった状態にあると見られる
よくある質問(FAQ)
Q1. ヤコビアン予想は「解決した」のですか?
現時点でそう書くのは不正確です。反例の Lean 形式化はビルドを通っていますが、査読論文もプレプリントも無く、PR もマージされていません。 数学の記録としては、まだ提出前の段階です。一方で「単なる SNS の主張」でもありません。§3 の表のとおり、段階を分けて理解するのが正確です。
Q2. 正標数(標数 p)では反例が昔から知られているのでは? それと同じ話ですか?
違います。今回の形式化された定理は、標数0の体を明示的に仮定した形(CharZero)で述べられています。さらに独立形式化のほうは任意の体で成立する形になっており、複素数体への特殊化も別の定理として用意されています。標数 p 限定の既知の現象とは別の話です。
Q3. 実ヤコビアン予想には1994年に Pinchuk 氏の反例があったはずですが、それと混同していませんか?
混同していません。今回の対象は実数体に限定されたものではなく、複素数体を含む形で述べられています。§2 の多項式は整数係数で、一致する2点の座標も有理数なので、有理数体・実数体・複素数体のいずれで考えても同じ2点が同じ像に写ります。
Q4. 2変数(平面)の場合はどうなりましたか?
未解決のままです。 形式化された PR の中でも、2変数の場合は証明が sorry(未証明)のまま、分類も「未解決」として残されています。今回の反例は3変数です。
Q5. Claude Fable 5 が証明まで書いたのですか?
ヤコビアン予想の件については違います。Fable 5 が生成したのは反例(多項式写像)で、Lean での形式化は Paul Lezeau 氏が手作業で行いました。ただし同じ時期の別の問題では、Fable が Lean ファイルへの自動形式化まで行った例が記録されています。
Q6. 素人が自分で確かめることはできますか?
反例の主張そのものは確かめられます。 多項式を偏微分してヤコビ行列式を展開し、2つの点を代入して像が一致するかを見るだけなので、厳密な有理数演算ができる環境があれば検証できます(§2 でも実施しました)。ただし浮動小数点で計算しないこと。 誤差で結論が変わります。
一方、「予想が本当に反証されたのか」の判断はそれとは別です。予想の形式化された文言が今回の PR で変更されている点も含め、数学の側の議論を待つ必要があります。
関連記事
- Claude Fable 5 はなぜ3週間止まったのか|輸出管理指示と再展開を一次情報で整理:同じモデルが主題の記事。公開3日後に米政府の輸出管理指示で停止された経緯を、Anthropic の公式発表だけで整理しています
- AIの「憲法」か国家の「合法」か|Anthropic排除とOpenAI合意の倫理的ジレンマ:Anthropic と米政府の関係を扱った記事
- DeepSeekはClaudeを「盗んだ」のか|蒸留攻撃とは何か、何がOKで何がNGか:モデルの出力から何が取り出せるのかという別方向の話
- GoogleのAnthropic投資400億ドルを解剖|資金還流とAIインフラ争奪戦の本質:Anthropic の資金調達と事業側の動き
- OpenAI×Microsoft提携を大改定|Azure独占終了・AWS Bedrock解禁の意味:AI 大手をめぐる契約・組織の動き
参考
- feat: add Jacobian disproof — google-deepmind/formal-conjectures PR #4474
- deancureton/jacobian — 独立した Lean 4 形式化
- Human mathematicians are being outcounterexampled(Kevin Buzzard 氏 / Xena Project)
- Levent Alpöge 氏による報告(X)
- On the origin of the Jacobian conjecture(arXiv:2512.23614)
- Formal Conjectures リポジトリ(Google DeepMind)