1995年に提起された数学の問題が新たな節目
1995年に提起された数学の予想について、数学者らと上海AI実験室のモデル「Intern-S2」の共同研究により、複素次元3を含む証明が得られた。その後、北京大学のチームが論文の主要な4つの定理をLeanで検証可能な証明に形式化した。Leanは数学的推論の正しさを検証するために設計されたコンピューターシステムだ。
目次
上海AI実験室は2026年10月15日、この成果を発表した。研究を主導したのは、大湾大学教授で同実験室の客員研究員でもある徐迪生氏。研究論文「Codimension-one holomorphic Anosov diffeomorphisms（余次元1の正則アノソフ微分同相写像）」は、スウェーデン王立工科大学（KTH）の張傑松氏を単独著者として記載している。
この成果は、フランスの数学者エティエンヌ・ギスの予想における余次元1の場合を解決し、複素次元3の場合も含む。これは運動と形状の間にある興味深い関係を扱う。特定の種類のカオス的な運動を支える空間が、それ自体、非常に秩序だった数学的構造を持たなければならないのかという問題だ。
Intern-S2は研究者との対話を重ねながら、アイデアや議論の展開を支援した。張氏はAI利用に関する申告書で、数学的内容をすべて独立に検証したと明記している。この共同研究では、機械による探索、人間の判断、そして独立した形式検証のプロセスが組み合わされた。
同実験室は、この成果を、これほどの水準の数学問題の解決に中国のAIモデルが貢献した初の事例としている。具体的な成果は分類定理であり、公開プレプリントと公開された形式化コードも伴う。
証明が示す運動と形状の関係
ギス予想は複素力学に属する。複素力学とは、座標が複素数の規則に従って変化するとき、数学的システムがどのように変わるかを研究する分野だ。複素数は2つの実数成分を持つため、複素次元3は局所的には実次元6に相当する。ここで扱う設定は、部屋の中を動く普通の物体よりも抽象的だ。
アノソフ系は、伸長と圧縮が正確に組み合わさった構造を持つ。運動を繰り返すと、ある方向では縮小し、別の方向では拡大する。各段階を支配する規則は厳密でありながら、近接した初期点が急速に離れ、カオス的な振る舞いが生じることがある。
形を繰り返し引き伸ばして折り畳む過程を思い浮かべるとよい。今回研究された数学的システムには、さらに厳しい条件が課される。伸長と収縮は一様な条件を満たし、運動は複素座標が与える構造を保たなければならない。
ギスは、コンパクトな複素多様体上のこうした系には、標準的な代数的記述が存在するはずだと予想した。多様体とは、全体の形状が複雑でも、小さな近傍では単純に見える空間のことだ。この設定でコンパクトであるとは、空間が無限に広がらないことを意味する数学的条件である。
張氏の定理によると、コンパクトかつ連結な複素多様体上の余次元1の正則アノソフ微分同相写像はすべて、複素トーラス上の双曲的自己同型写像と双正則共役である。平たく言えば、複素構造を保つ可逆な座標変換によって、その運動を非常に規則的な空間上の標準的な代数変換に移し替えられる。
複素トーラスは、複素空間内で周期的な格子の要素だけ異なる点同士を同一視して構成できる。複雑な力学系から、この整然とした幾何学的記述が導かれることが、この成果の核心だ。
対象範囲が重要な理由
論文が扱うのは余次元1の場合だ。この場合、収縮する部分または拡大する部分の一方が複素次元1となる。定理はこの限定された族を一般に扱い、複素次元3では予想を解決する。
ギスのより広い予想は、幅広い複素多様体上の正則アノソフ系を対象とし、複素インフラ・ニル多様体と呼ばれる空間上の標準的な代数モデルを用いて記述する。張氏の成果は、今回扱った場合について、複素トーラスと双曲的自己同型写像という、特に限定の強い答えを示す。
この問題に取り組む数学者にとって、この定理は、未知の空間と運動を特定する問題を、標準モデルの研究へと変える。座標変換によって元の系をそのモデルに結びつけつつ、複素幾何を保つことができる。
徐氏はこの問題を長年研究してきた。以前は、元指導教官でフィールズ賞受賞者のアルトゥール・アビラ氏とともに、3次元の場合を調べていた。徐氏と張氏はその後、関連する部分的な成果を得て、欧州数学会誌に発表した。今回の研究は、同じ数学的問題に長く取り組んできた成果の上に築かれている。
数学オリンピックから研究協力へ
Intern-S2の役割につながったのは、Intern-S1が2025年の中国数学オリンピックで挙げた先行成果だった。中国数学会の中等学校数学競技委員会は同年、AIテストを実施し、3つの中国製モデルに、人間の参加者と同じ制限時間内で問題を解くよう求めた。
Intern-S1は同じ採点基準で102点を獲得し、参加した3モデルの中で1位となった。金メダルの基準点は78点で、24点上回り、約31％高い得点だった。
徐氏はこのモデル系列を研究数学に活用できる可能性を見いだし、上海AI実験室は競技問題から未解決問題へと取り組みを広げようとしていた。両者の協力は2026年初頭に始まり、研究者とのやり取りやモデルの作業を整理する「Harness」と呼ばれるソフトウェアシステムの構築も含まれていた。
主な経緯は次の通り。
- 1995年：エティエンヌ・ギスが予想を提起。
- 2025年：Intern-S1が中国数学オリンピックのAIテストで102点を獲得。
- 2026年初頭：徐氏と上海AI実験室がモデル訓練の共同研究を開始。
- 2026年3月：徐氏が同実験室の客員研究員に就任。
- 2026年8月：内部開発版Intern-S2と支援システムが、集中的な数学的探索に使用される段階に到達。
- 9月29日：張氏の論文がarXivに投稿され、10月13日に改訂版が公開。
- 2026年10月15日：成果を公表。
数学者はどのようにAIを導いたか
Intern-S2がこの問題を最初に探索した際、約400ページに及ぶ導出報告書が作成された。徐氏は、元教え子でKTHの博士研究員を務める張氏に客員研究員として参加するよう呼びかけた。張氏は博士課程時代からギス予想を追っていた。
徐氏と張氏はモデルの提案を検討し、有望な切り口を見極め、次の探索を導くフィードバックを与えた。機械は推論の分岐を追い、議論を生成した。数学者はどの方向にさらに取り組む価値があるかを判断し、最終的な証明の構成を支援した。
同実験室によると、推論は7回に分けて継続された。その過程でモデルの問題グラフは15ノードから389ノードへ拡大し、累積出力は約1,000ページに達した。そこには数十のアプローチ案が含まれていた。
問題グラフとは、細分化された数学的課題とそのつながりを示す地図のようなものだ。あるノードが中間的な主張を表し、別のノードがその主張を証明するために必要な結果を表すこともある。報告された拡大は、システムが問題をどれほど細かく分割し、幅広く探索したかを示している。
張氏のAI利用に関する申告書には、完成した数学的内容についての責任が明記されている。内部版のIntern-S2が複数回の対話を通じてアイデアと議論の展開を支援し、張氏自身が数学的内容を独立に確認したという。また論文では、継続的な議論を行った徐氏に謝意を示している。
支援ソフトウェアが果たした役割
上海AI実験室は、長い推論の連鎖と繰り返される人間からのフィードバックを管理するためのソフトウェアをモデルと組み合わせた。このシステムは、難しい問題を小さな課題に分け、複数の方向を探索し、研究者が評価できる形で結果を返せる。
訓練手法は、幅広い科学的知識に、数学論文から集めた難問や、提案された解答を検証する方法など、研究数学を対象とする素材を組み合わせた。同実験室は、検証可能な報酬を用いた強化学習も説明している。これは、成功し、検証可能な推論が訓練の信号となり得ることを意味する。
研究者はその後、支援システムから得た経験を使ってモデル自体を改良した。実務上の目標は、長期にわたる研究を通じて有用な進展を維持することだった。中間結果を追跡し、新たな議論が展開する中で誤りを修正することも含まれる。
同実験室は、数学的推論に焦点を当てた評価であるIMO-ProofとAdvancedMathBenchの成果も挙げた。ギス予想のプロジェクトで、システムの動作を示す最も詳細な証拠は、大規模な導出、専門家のフィードバック、完成した論文、そして後続の形式検証という一連の記録だ。
北京大学はどのように証明を検証したか
董彬氏と劉若川氏が率いる北京大学のチームは、SHEAFフレームワークを用いて、張氏の論文の主要な4つの定理をすべて形式化した。議論の前提となるギスの結果も対象に含まれた。
形式化とは、数学的な定義、仮定、推論を、コンピューターが検証できる言語に置き換えることだ。通常の論文では、訓練を受けた読者がよく知られた手順を補って理解できることがある。Leanでは、その手順を厳密な命題と許可された論理演算で表現する必要がある。
チームの蒋杰東氏と呉彬氏によると、作業には約5日かかり、最大100のAIエージェントが並列で稼働した。約55万行のLeanコードが生成された。専門家は、形式化された命題が論文の主要定理の数学的意味と一致しているかも確認した。
SHEAFは、定義、命題、依存関係を有向グラフとして整理した。これにより複数のエージェントが相互に関連する部分に取り組むと同時に、どの命題に証明があり、どれが未完了なのかをチームが追跡できた。
形式化には、最終的な議論を置き換える以上の作業が必要だった。力学系のいくつかの補助結果は、既存の形式数学ライブラリに登録されていなかった。チームはその基礎を補うか、利用可能な既存の結果を使う方法を見つけ、各要素をつないで完全な証明の連鎖を構築しなければならなかった。
論文はarXivのプレプリントとして公開され、形式化コードはGitHubで公開された。発表では、学術誌への掲載や査読の判断については言及されていない。
2つの段階が一体となる理由
Intern-S2とSHEAFは異なる目的を担った。前者は数学的なアイデアや議論の探索を支援し、後者はLeanで検証可能な形式証明の構築を支援した。人間の数学者は探索を導き、得られた数学的内容を確認し、形式化された命題が意図した定理を表しているかを評価した。
作業の規模を見ると、この役割分担が具体的に分かる。約1,000ページの探索結果が研究論文につながり、その後の検証では約55万行の形式コードが生成された。それぞれの段階で、異なる目的に適した形式へと作業が変換された。
今後の研究者にとって、公開論文は数学的な議論を示し、公開コードは形式証明の構造を記録する。形式化の過程で追加された定義や結果も、同じ分野の後続研究の出発点となる可能性がある。
次の段階は再利用可能な検証モジュール
上海AI実験室は、この一連の手順を数学検証モジュールとしてまとめ、科学的発見プラットフォーム「Intern Duanyan」に組み込む計画だ。後続のプロジェクトが、モデルによる探索、専門家のフィードバック、形式検証を組み合わせた手法を再利用できるようにすることを目指す。
同実験室は、このプロジェクトを通じて開発した推論能力を、関連する数学的構造を持つ他分野にも応用する意向だ。研究問題を解き、有用な手法を再利用可能なソフトウェアにし、それを別の研究に活用するという循環を構想している。
徐氏にとって、この成果は大湾大学、上海AI実験室、KTH、北京大学の協力を通じて、長年の研究関心を発展させたものだ。より広い数学界にとっては、新たな分類結果であると同時に、人間の指導のもとでAIが研究に参加する過程を詳しく示す事例となる。
要点
- 新たな証明はギス予想の余次元1の場合を解決し、複素次元3も含む。
- 研究論文の単独著者は張傑松氏で、数学的内容をすべて独立に検証したとしている。
- 徐迪生氏と張氏は、繰り返しの探索とフィードバックを通じてIntern-S2を導いた。
- モデルの問題グラフは15ノードから389ノードへ拡大し、導出結果は約1,000ページに達した。
- 北京大学のSHEAFフレームワークは、主要な4定理と関連結果のLeanによる形式化を支援した。
- 検証作業には約5日かかり、約55万行のコードが生成されたという。
- 同実験室は、この一連の手順を再利用可能な数学検証モジュールにする計画だ。
