上海人工知能実験室（上海AI実験室）の訪問学者であり、大湾区大学の教授である許地生のチームは、書生科学多モーダル大模型S2（書生-S2）を利用し、「通専融合」技術プロセスに基づき、人間と機械の協力によって三次元Ghys猜想の証明を完成した。北京大学の董彬教授および劉若川院士のチームは、彼らが開発したSHEAFフレームワークを用いて、この証明の形式化検証を行い、この研究の正確性を確認した。 業界の人々は、これが中国の科学者が初めて中国の大規模モデルを使って世界的な数学の難問を解決したことを意味すると考えている。
「ギス猜想」は、フランスの数学者エティエンヌ・ギスによって1995年に提出されたもので、すべてのコンディショナル複素流形上の全純アノソフ系は、ある複素インフラ-パワーニングな流形上の全純射影同型に双全純対合するというものです。この問題は理論的な難しさと学問的意義を兼ね備えており、動力系分野の数学専門家によって、その分野で最も重要な長期的な公開問題の一つと認識されています。また、数学的な推論能力を試す重要な試金石とも言えます。
関連する論文はarXivのプレプリントプラットフォームに公開されており、その形式化コードもGithubプラットフォームで公開されている。
ギスの予想は、カオス系システムの「底層コード」を探すものである
1995年、フランスの数学者エティエンヌ・ギスがGhysの疑問を提出した。その核心は、カオスの動力系の行動が幾何学的な分類を決定するかどうかである。
これは複動力系分野における重要な難問です。もしこの仮説が正しいとすれば、混乱した動力学的軌道の問題を、簡潔で規則正しい標準代数学的モデルに「還元」することができます。
Ghysの証明をどう理解するか？境界のない、閉じた有限な空間で、各小さな領域が複素数算術の規則に従う「世界」を想像することができる。
アノソフ系については、生地をこねることに例えられます。圧迫、伸長、折りたたみによって、ある方向が引き伸ばされ、別の方向が圧縮されます。引き伸ばされる効果により、最初に隣接していた点が迅速に分離します。初期条件のわずかな違いが、全く異なる進化結果をもたらすのです。
ギスの仮説によると、「生地を混ぜるような動きでありながら完全に規則的」な動きが存在する限り、その「世界」は単純な規則によって何度も組み合わせられ、結晶格子のように非常に整った形態になるだけだ。例えば複素環面である。
別の視点から見ると、この運動は本質的に「世界」の単純な平行移動、回転、または拡大縮小に他ならない。つまり、運動の様式があまりにも混沌としているため、世界がどのような形になるかを逆に決定するのだ。 2026年国際数学者大会45分間の報告者である、北京大学北京国際数学研究センターの謝俊逸教授は次のように評価した。「Ghysの疑問の難点は、その対応する実数版の類似の断言が依然として有名な完全に公開された難問であること、複素数のケースはより厳格になり、複素動力系の厳格性の研究において重要な問題であり、非常に困難である」と。
大湾区大学の教授である許地生は、この仮説の研究に長年携わってきました。彼は指導教官でありフィールズ賞受賞者であるアヴィラ教授と協力して3次元の場合について研究しましたが、有効な証明のアプローチを確立することはできませんでした。その後、彼は学生の張潔松博士と協力して3次元の場合におけるGhys仮説の部分的な弱関連結果を得ました。この成果は数学のトップジャーナルである「JEMS」に掲載されました。
7班の連続シミュレーション、389個のノードで、人間と機械が協力して重要な突破を達成
「科学の発見は、知能に対する最終的な試練である。」上海人工知能研究所の所長でありチーフサイエンティストである周伯文は次のように述べています。問題が古く、基本的なものほど、AIが効率を高める余地が大きいという。AIが関与する単クローン抗体の生成、タンパク質の折りたたみ、そして今も解決できないミレニアンの難問であるナヴィ・ストークス方程式など、すべてこの法則に当てはまります。3次元Ghysの仮説も、このような基本的な難問の一例です。
2026年3月、許地生教授が上海AI実験室の訪問学者となりました。これにより、上海AI実験室との科学研究の協力がより深く、より密接な段階へと進みました。両者は共同チームを結成し、数学研究の場向けにHarnessシステムを同時に構築しました。許地生教授は数学の科学研究経験を活かし、モデルとシステムの能力の不足点を正確に指摘しました。実際の先端的数学研究課題に基づき、システムが複数回のイテレーションを経て改善されるようにしました。
8月、内部で開発された書生-S2および対応システムは、大規模な再帰的推論能力を持ちながら、高い柔軟性のある人間とコンピュータのインタラクション能力も備えています。複雑な数学問題の処理能力において、質的な飛躍を遂げています。特に、3次元Ghys猜想に対する最初の推論では、書生-S2が400ページに及ぶ推論報告書を生成しました。
訓練戦略の面では、研究チームは「通専融合」技術路線を堅持し、大規模な科学知識の事前訓練によってモデルの基盤を固めた上で、研究レベルの後期訓練データを丁寧に構築している。これには、数学論文から得られる大規模な難問や信頼性の高い検証方案が含まれ、モデルの研究レベルにおける数学分野での専門性、厳密性、規範性を向上させている。
アルゴリズムの訓練面において、研究チームは非同期長距離推論強化学習の訓練方法を突破し、検証可能な報酬の下で誤差の指数級的な蓄積、長期状態の維持、自己修正といった一連の根本的な難問を解決した。また、Harnessがもたらす能力向上をモデルに逆方向にディープレンシングする自己進化アルゴリズムも開発し、モデルの直接推論の能力を超える高度な問題において、有効な監視信号を継続的に得ることで、モデルの能力の自律的な向上を促進した。
IMO-ProofやAdvancedMathBenchなどの、長期的かつ厳密な推論を重視する競争数学および高等数学の基準において、書生-S2は全体的に既存のオープンソースモデルをリードし、一部の指標ではGemini 3.1 Proなどのトップクラスのクローズドソースモデルを上回り、世界で最も長期的な推論能力が高いオープンソースモデルに数えられる。
これで、書生-S2の基模能力は、科学研究チームが研究レベルの数学問題を解決するための基本的な水準に達している。しかし、世界級の難問を本当に解くには、さらに一層の努力が必要だ。チームは、突破の鍵はより密接な人間と機械の協力にあると考えている。
書生-S2及び対応システムは、長いチェーン型の大規模な推演の利点を活かし、複数の支線を同時に試行し、複雑な問題を分解し、異なるアプローチを考える。大量の煩雑な推論作業を引き継ぎ、各イテレーションで大量の試行結果が得られる。研究者は大まかな方向性を把握し、どのアプローチが深く掘り下げる価値があるか、どの道が行き止まりかを判断し、直感的な提案を行い、それをシステムの次のイテレーションの指針とする。 二人は一方的な独立した推論ではなく、人間とコンピュータが協力して、複数回の対話とフィードバックを通じて、密接な相互作用の中で反復的に進められる。
図中には、システムの複数回の相互作用プロセスと、各相互作用における再帰的求解構造が示されている。ここで、エッジは子問題の分解関係のみを表し、文脈依存関係を表していない。各ノードは、そのノードより前の時系列上の全てのグローバルコンテキストにアクセスできる。
AIが提供した最初の探索基盤の上で、数学者である許地生と張洁松は重要な突破点を鋭く見極め、モデルにフィードバックを続け、探索の方向を調整し、価値あるアプローチへとモデルを深めるように導いた。研究を進める過程で、書生-S2は7回にわたって連続的な推演を完了し、問題図は15個のノードから389個に拡大し、数千ページに及ぶ厳密な証明を生成し、数十種類の新しい論理的アプローチも生み出した。これにより、チームはこの世界的な数学の難問を解決することに成功し、その分野の国際的な先駆学者から「思考の深さが予想を大幅に上回っている」という評価を受けた。
興味深いことに、論文がarXivのプレプリントサイトに掲載される前に、前述の動力系専門家である謝俊逸教授もGPT-6を使ってこの問題に挑戦しましたが、証明方法を見つけることができませんでした。「これは、書生-S2がこの先端的数学研究において持つ独特の価値を証明するだけでなく、中国の大モデルも先端的数学の舞台に立ち、世界的な難問の解決に貢献できるというメッセージを伝えています。」
北大チームが専門的な形式化検証を提供する
AIの支援による成果は、検証に耐えうるか？
北京大学の董彬教授と劉若川院士のチームは、この論文の全4つの主要定理の形式化検証を完了し、Leanの検査を通過した。Leanは対話型定理証明システムであり、形式化証明に対して厳密な論理検査を行うことができる。北大のチームの核心メンバーである姜杰東と吴彬は、全プロセスがわずか5日で完了し、ピーク時の同時処理数が100個のスマートアイドルに達し、約55万行のLeanコードが生成されたと述べた。これは非常に大きな並行規模と極めて速い検証速度を示している。 専門家が、形式化された述べ方と論文の主要定理の意味内容が一致していることを確認し、Lean検証の証拠によりその厳密な正確性が保証される。
形式化の難しさは、まず数学そのものに由来する。自然言語の証明は読者が持つ数学的知識によって条件や推理を補完されることが多いが、形式化ではそれをコンピュータが確認できる完全な証明として実現しなければならない。論文で引用されている結果が基礎定理ライブラリに含まれていない場合は、形式化された証明を追加するか、既存の結果を利用する代替方法を見つける必要がある。特に動力系の分野では既存の形式化基盤が不足しており、今回の作業で多くの基盤が補完され、論文が依存する多数の文献結果をカバーしている。 研究レベルの数学において、これらの作業には定義の正確な表現、証明構造の分解、数学的ツールの選択が関わる。多数のスマートアイテムが並行して動作する場合、各部分の定義、述語、依存関係が互いに連携していることを確保しなければならず、そうすることで完全な証明チェーンが構成される。
このプロセスを組織するために、北大のチームは自ら開発したSHEAFフレームワークを使用した。複数のアイドルが、論文内の命題、定義、依存関係を、目標定理から基礎定理ライブラリへと層ごとに拡張される有向非環図として整理する。モデルはこのフレームワークの中で命題分解や形式化証明の構築に参加し、チームはこの図を中心に作業を進め、各ノードの述語、証明、剪定状態を追跡し、大規模な形式化タスクを相互に関連し、検証可能なステップに分解する。
2021年、大規模モデルがまだ登場していない時期に、北京大学北京国際数学研究センターの董彬教授のチームは、人工知能が数学研究のパラダイムを再構築することに気づいていました。 北大数学チームは、国際的に最も早く「数学のためのAI」分野の研究を展開したチームの一つです。FATEという高度な評価データセット、Matlas/LeanSearchによる大規模な数学知識検索、Rethlas/Archon/Danus/Iterisによる自動推論と形式化検証を含む完全な技術チェーンを構築しています。彼らが開発したAIシステムは、アンダーソン問題という公開された数学的難問を解決することに成功し、国内初であり、国際的にも初となる、大学チームが人工知能を活用して重要な数学的疑問を独自に解決した成果となりました。 最近、チームはまた、ポアンカレの予想の形式化検証を独立して完了しました。
単一の難問を解決することから、科学研究の基盤設備まで
この研究の意義は、新しい科学研究のパラダイムを検証することにもある。伝統的な数学研究は個々の天才による長い探求に依存しているが、今回の研究では専門家の直感を機械的な解決プロセスに体系的に組み込むことで、「システム探索—専門家の判断—成果の蓄積—フィードバックと修正」という閉環を形成した。このパラダイムは、「探索空間が広大であり専門家が不足している」基礎研究分野に複製・普及することができ、より多くの「0から1への」革新的な突破を実現することができる。
次に、この研究で実現された完全な能力の閉環を基に、チームは書生・端砚科学発見プラットフォームの再利用可能な数学検証モジュールにまとめ上げ、後の科学問題研究で直接利用できるようにする。 同時に、3次元Ghysの猜想の突破を出発点として、上海AIラボは蓄積された推論能力を数学構造が共通する他の学問分野にも応用していく。新たな突破を達成した後、その新しい推論能力を端砚プラットフォームに再封入し再利用することで、さらに多くの学問分野と融合し次の段階の突破を目指す。「突破—封入—再利用—再突破」という自己進化のサイクルを形成する。雷峰網（公式アカウント：雷峰網）もこの方向における最新の進展を継続的に追跡していく。
雷峰網のオリジナル記事は、許可なく転載することを禁じられています。詳細は転載に関する注意事項をご覧ください。