31年越しのGhys予想、複素3次元で証明　上海AI研究所のIntern-S2が支援

上海人工知能研究所は2026年10月15日、科学研究向けAIモデル「Intern-S2（書生-S2）」を活用した数学者との共同研究で、Ghys予想の複素3次元の場合の証明に至ったと発表した。1995年に提起された予想について、複素3次元を含む「余次元1」の場合を扱う論文が公開され、北京大学の別チームが主要4定理を証明支援系Leanで形式化した。

論文の単独著者は、スウェーデンのKTH王立工科大学に所属する博士研究員の張潔松（Jiesong Zhang）氏だ。張氏は、Intern-S2の内部版との複数回の対話を通じて数学的な着想や議論を発展させ、すべての数学的議論を自身で確認したと記している。

■カオスを生む運動から空間の形を分類する

Ghys予想の出発点は、フランスの数学者エティエンヌ・ギスが1995年に学術誌Inventiones Mathematicaeへ発表した論文「Holomorphic Anosov systems」にある。ある種のカオス的な運動が存在することから、その舞台となる空間の幾何学的構造をどこまで決められるかを問う問題だ。

対象となるアノソフ微分同相写像は、接空間を安定方向と不安定方向に分け、反復によって前者を一様に収縮させ、後者を一様に拡大させる。名称はソ連の数学者ドミトリー・アノソフに由来する。同氏は1967年、負曲率を持つ閉リーマン多様体上の測地流について、体系的な研究を発表している。

これに複素構造を保つ「正則」という条件が加わると、取り得る幾何学的構造が強く制約される。Ghys予想は、コンパクト複素多様体上の正則アノソフ微分同相写像が、複素インフラニル多様体（complex infra-nilmanifold）上のアフィン自己同型と双正則共役になるというものだ。双正則共役とは、逆変換も正則な座標変換によって、二つの運動を対応させられることを意味する。

この予想の核心は、複雑な軌道を持つ運動を、代数的なモデルとして分類することにある。ギスは複素2次元の複素曲面の場合を証明していたが、より高い次元での分類が研究課題として残っていた。

■余次元1の証明が複素3次元をカバー

張氏の論文が扱うのは、安定部分束と不安定部分束のいずれかの複素次元が1となる「余次元1」の場合だ。コンパクトで連結な複素多様体について、この条件を満たす正則アノソフ微分同相写像が、複素トーラス上の双曲的自己同型と双正則共役になることを示した。

複素トーラスは、複素ベクトル空間で格子の周期だけ離れた点を同一視して得られる空間だ。今回の定理は、対象の空間自体がこの複素トーラスと双正則同型になり、その上の運動も標準的な代数的モデルに変換できることを述べている。

複素3次元では、安定・不安定の両部分束がともにゼロでないことから、その次元は1と2に分かれる。このため、余次元1についての定理が複素3次元の場合全体をカバーする。より高次元の一般の場合は、引き続き未解決の研究対象となる。

証明の難所の一つは、空間の位相的な形と複素構造の違いにある。張氏の論文によると、複素3次元以上では実トーラスと同相な空間にも非標準的な複素構造が存在するため、位相的な分類から双正則な分類へ進むための議論が必要になる。

論文は、まず位相的な分類を示し、不変部分束の正則性を確立したうえで、複素構造を保つ分類へ進む構成を取る。プレプリント「Codimension-one holomorphic Anosov diffeomorphisms」は2026年9月29日にarXivへ投稿され、10月5日の改訂を経て、10月13日の第3版でAI利用の申告と形式化についての説明が追加された。

■7回の反復で数学者が探索を方向付け

上海人工知能研究所の発表で共同研究を率いた人物として挙げられるのは、広東省東莞市の大湾区大学教授で、同研究所の客員研究員でもある許地生（Disheng Xu）氏だ。張氏は北京大学で許氏らの指導を受けて博士号を取得し、KTHで博士研究員を務めている。論文では許氏との継続的な議論と、上海で研究に取り組む機会への謝意を示している。

研究所の説明によると、許氏は2026年3月に客員研究員となり、数学研究向けの「Harness」と呼ぶ支援システムを共同チームで構築した。8月には、内部で改良したIntern-S2と周辺システムが、大規模な推論と柔軟な対話を進められる段階に達したという。

AIは複雑な命題を分解し、関連文献を調べ、複数の証明方針を並行して探索した。数学者は出力を読み、有望な着想を選び、行き詰まった経路を見極め、次の探索への指針を与えた。研究所は、汎用的な推論能力と専門知識を組み合わせるこの方法を「通専融合」と呼んでいる。

研究所発表では、最初の推論で約400ページの報告が生成された。その後の協働を含む7回の接続的な推論を通じ、命題や部分結果の関係を示す問題グラフは15ノードから389ノードへ拡大し、導出の総量は約1000ページに達した。数十種類の論証方針も生成したという。

同研究所は、この成果を、中国の大規模モデルを使って世界的な数学の難問を解いた初の事例と位置付けている。また、同分野の研究者から、思考の深さが予想を超えたとの評価を得たとしている。張氏の論文では、数学的議論と論文全体について著者自身が責任を負うことを明記した。

■主要4定理をLeanで形式化

証明の形式化を担当したのは、北京大学の董彬（Bin Dong）教授と劉若川（Ruochuan Liu）教授のチームだ。同チームが開発した自動形式化フレームワーク「SHEAF」を使い、主定理Aと、それを支える定理1.1、1.2、1.3、および論文が利用するギスの結果をLeanで扱える形にした。

形式化と最終的な定理の人的確認は、Jiedong Jiang氏とBin Wu氏が担当したと論文に記されている。上海人工知能研究所によると、作業には約5日間を要し、最大100のAIエージェントが並行して稼働した。生成したLeanコードは約55万行に上るという。

Leanでは、数学的な対象の定義、定理の条件と結論、証明を形式言語で記述する。小さな検査プログラムであるカーネルが、明示された前提から結論が導かれることを確認する。一方、形式言語で書かれた定理が論文の主張に対応しているかは、専門家が確認した。

公開リポジトリの説明では、4定理のうち主定理A、定理1.1、定理1.3は、ホモトピー型がトーラスと等しい閉多様体の位相的剛性に関する既存定理を、明示的な仮定として受け取る。この結果はHsiangとWallが1969年に証明したもので、今回の形式化では外部から与える数学的な入力として扱われる。定理1.2はこの仮定を使わずに検証される。

コードはGitHubのHolomorphicAnosovリポジトリで公開されている。READMEには、Lean v4.35.0-rc1を指定した環境と、ライブラリのビルド、定理の比較検査を実行する手順が示されている。SHEAF自体も公開され、命題とその依存関係をグラフで管理しながら形式化を進める仕組みを説明している。

■積み上がる形式数学と検証の基盤

Leanは、レオナルド・デ・モーラ氏がMicrosoft Research在籍中の2013年に始めたプロジェクトだ。Lean 4.0は2023年9月に正式公開され、同年7月に設立された非営利のLean Focused Research Organizationが開発を支えている。

数学ライブラリMathlibには、定義や既存の定理が蓄積されている。コミュニティの公式統計では、2026年10月18日確認時点で定理29万502件、定義13万9391件を収録する。新しい証明の形式化では、こうした基盤を再利用できる。

先行例には、クラウゼンとショルツの研究に関する「Liquid Tensor Experiment」がある。Leanコミュニティは2021年に主要な中間成果を報告し、2022年7月に課題全体の形式化完了を発表した。2023年には、テレンス・タオ氏らの多項式フレイマン＝ルーザ予想の証明も、共同プロジェクトで約3週間かけて形式化された。

形式検証の信頼性を支えるソフトウェアも、継続的に検査・改良されている。デ・モーラ氏の報告によると、2026年7月には、コラッツ予想の反証を装ったコードをきっかけに、入れ子の帰納型を扱うLeanカーネルの不具合が特定され、修正された。同氏は8月にも追加の調査結果を公表している。

今回公開された証明と定義は、正則アノソフ系に関する今後の形式化でも参照できる資産となる。証明を探索する工程と、前提・結論・推論を明示して検査する工程を組み合わせた点が、この研究の特徴だ。

■公開モデルと研究用内部版、それぞれの役割

Intern-S2は、上海人工知能研究所が2026年9月13日の第19回浦江イノベーションフォーラムで発表した科学向けマルチモーダルモデルだ。研究所は公開モデルと試用サービスを案内しており、Hugging FaceでもIntern-S2系列のモデルが提供されている。張氏が論文で利用を申告したのは、その内部版である。

開発チームの技術資料では、基礎モデルのパラメーターを固定したまま、専門知識を補うMemory Decoderを組み合わせる方法を説明している。補助モデルと基礎モデルが同じ文脈を並行して処理し、その予測を統合する設計だ。専門領域ごとの知識を拡張する手段として研究されている。

上海人工知能研究所は、数学論文に基づく研究水準の課題や検査方法を後段の学習に取り入れ、非同期の長期推論向け強化学習などを用いたと説明する。数学者との協働で見つかったモデルやシステムの弱点も、改良へ戻す開発の循環を設けたという。

研究所発表では、IMO-ProofやAdvancedMathBenchなどで、Gemini 3.1 Proを含む上位モデルに匹敵する性能を示したとしている。これらは開発側による評価である。AdvancedMathBenchの公開資料は、大学学部・大学院の資格試験水準の数学を対象に、自然言語による証明の生成と検証を評価するベンチマークと説明している。

証明生成の過程を詳しく研究するには、使ったモデルの版、対話履歴、探索を管理するシステムの設定も重要になる。今回の論文にはAI利用の申告があり、研究所発表には反復回数や探索規模が示された。数学的な結論については、論文と形式化コードを対応させて検討できる形が整えられている。

■国際共同研究を支える組織と法制度

上海市の公表資料によると、上海人工知能研究所は2020年7月に発足した。共同研究者の許氏が所属する大湾区大学は、2025年6月に中国教育部から設立承認を受け、同年9月に最初の学部学生を迎えた大学だ。張氏の論文上の所属は、ストックホルムのKTHである。

中国の研究機関とのデータ共有やサービス利用では、適用される法制度も検討事項となる。2017年制定の国家情報法第7条は、組織と公民に対し、法に従って国家情報活動を支持し、援助・協力することを求める。同法第8条は、情報活動を法に基づいて行い、個人と組織の合法的な権益を守ることも定めている。

2021年制定のデータセキュリティ法第24条は、国家安全に影響する、または影響する可能性があるデータ処理活動の安全審査を規定する。第35条では、国家安全の維持や犯罪捜査のために公安・国家安全機関がデータを取得する際、厳格な承認手続きを経て法に従って行い、関係する組織や個人が協力すると定めている。

2026年1月施行の改正サイバーセキュリティ法は、第30条でネットワーク運営者の捜査等への技術的な協力を規定する。第39条の国内保存義務は、重要情報インフラ運営者が中国国内で収集・生成した個人情報と重要データを対象とする。共同研究では、扱うデータ、サービスの運営形態、越境移転などに応じて条件を確認する必要がある。

■証明の発見から理解と再利用へ

AIと数学を巡っては、成果の生成と人間による理解をどう両立するかという議論も進んでいる。カーネギーメロン大学のジェレミー・アビガド氏は2026年の論考で、AIが形式的・非形式的な双方の方法で研究水準の定理を証明する進展を指摘し、数学者に技術の動向と機会・課題への対応を促している。

タオ氏は10月の講演「Math 2.0」で、AIによる未解決問題の自動解決への過度な集中を論じた。そのうえで、AIを数学の共同体や、実社会での応用を支える数学的理解の維持・発展に役立てる将来像を示している。

トロント大学のダニエル・リット氏も9月の論考で、出自を問わず興味深い数学的成果を歓迎するとともに、成果を生み出すことと数学を理解することを、それぞれ評価する必要性を述べた。これらは、AIが数学研究へ参加する時代の研究・教育のあり方を巡る議論だ。

上海人工知能研究所は、今回の協働から得た能力を、科学発見プラットフォーム「書生・端硯」の再利用可能な数学検証モジュールへ発展させる方針を示す。同プラットフォームは、生命科学、材料、量子分野などで、科学モデル、専門エージェント、実験データ、実験装置を結ぶ構想を掲げている。

今回の研究では、数学者が問いと探索方針を定め、AIが候補となる議論を広げ、著者による確認と別チームの形式化が続いた。複素3次元で得られた分類結果に加え、この協働の進め方と公開された証明基盤が、次の研究を組み立てる手掛かりとなる。

元記事: Chinese AI Model Helps Prove 31-Year-Old Math Conjecture With Machine-Verified Lean Proof