ヤコビ予想が3次元で崩れた、AIが強いのは反例の発見

Terence Tao, “A digestion of the Jacobian conjecture counterexample”（2026年7月21日）。査読を経た論文ではなく、本人のブログ記事である。反例は複素3次元空間から複素3次元空間への7次の多項式写像で、ヤコビ行列式は定数 −2、それでも大域的に可逆ではない。非単射性は F(0,0,−1/4) = F(1,−3/2,13/2) = F(−1,3/2,13/2) = (−1/4,0,0) という3点の衝突で示される。探索の難しさについては、7次の写像ならヤコビ行列式は $3 \times 6 = 18$ 次までの多項式になりうるので、非定数項がすべて消えるのは $\binom{18+3}{3}-1 = 1329$ 本の方程式が成り立つことに等しく、3次元の7次多項式写像がもつ $3 \times \binom{7+3}{3} = 360$ の自由度よりはるかに多いとして、“So finding such a polynomial looks highly unlikely to be located by brute force.” と書く。Taoは記事本文ではこの結果を “recently shown (using the Fable AI)” とだけ書き、Claude にも Levent Alpöge にも触れていない（本文の全文検索で0件、両名が現れるのはコメント欄のみ）。発見者名の典拠は²と⁴である。自身の記事は “digestion exercise” で、代数幾何をほとんど使わず “miracles” を最小化する方針だとする。計算のいくつかの確認にAIチャットボットを使ったとも明記する。予想は2次元では未解決のままで、1次元では容易に示せるとする。https://terrytao.wordpress.com/2026/07/21/a-digestion-of-the-jacobian-conjecture-counterexample/ ↩ ↩² ↩³ ↩⁴ ↩⁵ ↩⁶ ↩⁷ ↩⁸ ↩⁹ ↩¹⁰

Melissa Lee（Monash University）, “‘hello there the jacobian conjecture is false thanx’: why a tiny social media post has mathematicians rethinking AI”, The Conversation（2026年7月22日）。研究論文ではなく、研究者が一般向けに書いた報道記事である。Alpöge が Anthropic の Claude Fable 5 を用いて反例を見つけ、それは “short enough to fit into a single X post” だとする。困難は入り組んだ構成や長い証明ではなく、正しい性質を持つ1つを見つけるために可能な多項式写像からなる巨大な探索空間をどう歩くかにあった。Alpöge がAIモデルにどうプロンプトを与えたかの詳細は公開されていないと明記している。証明の側の歴史については、“the Jacobian conjecture has been the subject of many claimed proofs, including by Beniamino Segre and Wolfgang Gröbner, two famed 20th-century mathematicians. However, in each case, subtle errors were found that invalidated the arguments.” とし、反例の側については “The brevity of the counterexample made it easy for other mathematicians to verify.” とする。予想の性格として “in theory, it should be easy to find a counterexample” を挙げ、2017年の Math Stack Exchange の投稿から “for all what we know, some smart undergraduate can simply write a formula […] that will be a counter-example to this conjecture” を引く。2次元については “Computational results have also shown it is true in two dimensions for polynomials up to degree 100” と記す。https://theconversation.com/hello-there-the-jacobian-conjecture-is-false-thanx-why-a-tiny-social-media-post-has-mathematicians-rethinking-ai-283883 ↩ ↩² ↩³ ↩⁴ ↩⁵ ↩⁶ ↩⁷ ↩⁸ ↩⁹ ↩¹⁰ ↩¹¹

Kevin Buzzard, Xena Project blog, “Human mathematicians are being outcounterexampled”（2026年7月20日）。査読を経ていないブログ記事である。ChatGPTの「Sol」やClaudeの「Fable」といったAIが、短い期間に複数の長年の予想を反例で覆すか解決した経過を記録する。Erdős の単位距離予想では ChatGPT が証明を生成し、数日のうちにAIが Lean で形式化した。Grothendieck の60年来の問いでは、7月7日に話題に上り11日に反例の報告が届いた（4日）。なおブログ中の「2週間」はこの件ではなく、別の研究者が250K行のLeanを書いた期間である。ヤコビ予想の反例はワールドカップ決勝の最中に見つかった。“machines seemed to be getting very good at finding counterexamples” と書く。反例が “low-hanging fruit right now” かもしれないという一節は、Akhil Mathew がそう深く理解していたようだ、という形で書かれている。記事本文には、反例（存在命題）と普遍命題の証明を切り分ける議論は無い（本文の全文検索で “existence” “universal” “deep reasoning” “fundamentally” “for all” “there exists” とも0件）。この切り分けは同記事のコメント欄にあり、Buzzard 本人（投稿者アカウント xenaproject、2026年7月25日）が “No — there’s a genuine difference between a proof of the Jacobian conjecture and a proof of its converse. For example, it is extremely unlikely that a proof of the conjecture would have fitted into a tweet. The conjecture is a “for all” statement, its converse is a “there exists” statement.” と述べている。自然言語出力の信頼性の低さを認めた上で、非形式なAI生成証明を読むことを拒み Lean による形式検証を要求する。博士課程の学生も月200ドルを払うべきだという発言には、コメント欄で公平性・アクセス格差と数学の脱技能化をめぐる批判が出た（本文には批判は無く、“de-skill” “equity” “afford” いずれも本文0件）。利害については記事本文が自ら開示している——ワークショップは自動形式化ツールを持つ Logos Research の資金提供を受け、Buzzard 自身が参加者25人に Claude Max 購読を買い、OpenAI は参加者全員に ChatGPT Pro の無償アクセスを提供した。Erdős の完全形式化を行った Boris Alexeev は “works at OpenAI”、Buzzard 自身は mathlib について “declaration of conflict of interest: I am a maintainer” と記す。https://xenaproject.wordpress.com/2026/07/20/human-mathematicians-are-being-outcounterexampled/ ↩ ↩² ↩³ ↩⁴ ↩⁵ ↩⁶ ↩⁷ ↩⁸ ↩⁹ ↩¹⁰ ↩¹¹

David Speyer, Secret Blogging Seminar, “The new counterexample to the Jacobian conjecture”（2026年7月20日）。査読を経ていないブログ記事とそのコメント欄である。写像を “generically three to one, not bijective”、ヤコビ行列式は定数 −2 と説明する。“Levent Alpöge tweeted that Fable had found a counterexample” と記す。Will Sawin は “ChatGPT prompted by Andy Jiang” が “almost an elegant geometric construction” に近いものを出したとし、対称積空間による記述を与える。19歳のハーバード大学生 William Thompson は “with substantial assistance from GPT-5.6 Sol” 後続の仕事を行い、“two separately implemented exact verifiers” の独立な一致を確認した上で、優先権も大域的最小性も主張せず、より早い明示的な立方斉次簡約が既知かどうか意見が欲しいと留保する。Shubhodip Mondal は Picard 群の計算について “According to GPT” としつつ “I did not check carefully” と付記する。Will Sawin が「代数幾何学者が頭の中で、非自明な計算をせずに検証できる証明」を目標として掲げ、Jake Levinson が座標に依存しない幾何学的議論を寄せている（Speyer 自身の寄与は点の数え上げと座標計算。$\mathrm{Cl}(U)$ の消滅を使う明示的な excision 完全系列はコメント投稿者 Skooi によるもので、Speyer 自身も class group についての観察を Skooi に帰している）。コメント欄には後続の波及も記録されている——7月23日に Alexander Dvorsky が一般化消滅予想 GVC(5) への5変数の反例を、7月24日に別の投稿者が Zhao の消滅予想への明示的な反証物を “Two independent exact verifiers” と公開リポジトリつきで、7月27日に royvanrijn が像予想への反例（展開して8項）を、同日 hexianmeng が「5変数・全次数14・Hessian行列式は定数128」で Hessian 予想 HC_5 を反証する論文（arXiv:2607.22198）を投稿している。Dvorsky の主張については Speyer が検算して合わないと指摘し、Dvorsky が検証コードを示した結果、Speyer 自身が $ad+bt$ を $ad+bc$ と写し間違えていたことが同日中に判明した。https://sbseminar.wordpress.com/2026/07/20/the-new-counterexample-to-the-jacobian-conjecture/ ↩ ↩² ↩³ ↩⁴ ↩⁵ ↩⁶ ↩⁷ ↩⁸ ↩⁹ ↩¹⁰

Jasper Dekoninck, Ivo Petrov, Kristian Minchev, Mislav Balunovic, Martin Vechev ほか, “The Open Proof Corpus: A Large-Scale Study of LLM-Generated Mathematical Proofs”（arXiv:2506.21621, 2025年6月23日投稿／2026年1月14日改訂）。査読前のプレプリントである。最先端のLLMが生成した 5,000件を超える人手評価済みの証明を扱い、(1) 自然言語による証明生成と形式証明生成の性能差、(2) 最終解答の正答率と証明全体の妥当性の食い違い、(3) best-of-n 選択が証明の質に与える影響、の3点を調べる。誤りの割合は本文2ページ目の Key findings に出ており、“the OPC generally consists of 43% correct proofs” とする。同じ段落は “While GEMINI-2.5-PRO loses only 8% of its final-answer accuracy when proof correctness is required, O3 suffers a drop of almost 30%.” と述べ、5.4節では MathArena 部分集合について “O3 performs notably worse, with only 59.5% of its answers containing a correct proof. This substantial difference between models shows that final-answer accuracy is not a reliable indicator of proof generation capability.” とする。証明の正しさの判定では GPT-5 が最も高く、5回の多数決で90.8%（単発では89.3%）、人間の基準は90.4%である。著者らが追加学習した80億パラメータのモデルは同じ条件で88.1%に達し、Gemini-2.5-Pro と並ぶ。なお arXiv の要旨ページは v2 を指していても v1 の要旨（この8Bモデルを「最良モデルである Gemini-2.5-Pro と同等」とするもの）を返す。v2 のPDF本体の要旨は “matches GEMINI-2.5-PRO, and performs close to the best model, GPT-5” に書き換わっており、本稿の記述はPDF本体で確認した。https://arxiv.org/abs/2506.21621 ↩ ↩² ↩³ ↩⁴ ↩⁵

Martin Balko, Jan Grebík, Pavel Hubáček, Martin Koutecký, Matěj Kripner, Václav Rozhoň, Robert Šámal, Adrián Zámečník, “Bolzano: Case Studies in LLM-Assisted Mathematical Research”（arXiv:2604.16989, 2026年4月18日投稿／4月24日改訂）。査読前のプレプリントである。数学と理論計算機科学の 8つの問題で新しい結果を出したとし、8つのうち6つが出版に値する研究の水準に達し、8つのうち5つは実質的に自律的に生成されたと報告する。評価には Feng らによる有意性と自律性の分類を用いる。作業の種類ごとの内訳は本文1ページ目にあり、“it was particularly good at finding counterexamples and obstructions, proposing concrete constructions and gadgets, or extending a known base case or simpler proof template to a more general statement” とする。3ページ目の総括は “LLMs excel at generating proof candidates, constructing counterexamples, and making cross-domain connections. In early 2026, human guidance remains relevant for problem selection, high-level strategy, and verification.” であり、限界として “it is hard to cleanly disentangle the human and AI contributions; even selecting the right problem to work on is a nontrivial human input” を挙げる。8問題のうち5番目（Combinatorics）は “We disprove a conjecture on function-preimage partitioning from the KAMAK 2020 workshop” と明示され、付録Cに Theorem 11 (Counterexample to the original conjecture) として証明がある。2ページ目の Table 1 はこの反証（Partitioning, Section 3.5）を自律（A）列かつ Minor novelty 行に置く（Negligible novelty 行は空である）。8問題のうち1番目では人間が解析の方針を、3番目では人間が protocol の変種と簡単な基礎ケースの証明を与えている。https://arxiv.org/abs/2604.16989 ↩ ↩² ↩³ ↩⁴ ↩⁵ ↩⁶ ↩⁷