Ghys予想の複素3次元の場合をAIの助けで証明、Leanで検証、査読は確認できず

悠 Yu NiiboriAIエンジニアプロフィール

要点

対象：AIが数学の難問を解いたと聞いて気になった人

数学者のJiesong Zhang氏が、ギス予想（Ghys予想）の複素3次元の場合を証明した論文を、2026年9月29日にarXiv（査読を受けていない論文も載る論文公開サイト）に投稿しました。¹

この記事の目次（4節）

10月13日の改訂版で、AIの使用の申告が加わりました。上海AI研究所のAI「Intern-S2」の社内版と何度も対話して考えを進め、証明の中身はすべて自分で確かめた、と書いています。¹²

証明は、人が方向を決め、AIと対話を重ねて進めたものです。論文の主な定理はLeanで機械検証されましたが、論文が査読を受けたという記述は見つかりませんでした。

AIに仕事を任せる人にとっての見どころは、確かめ方と責任の置き方です。

証明されたのは何か

ギス予想は、ある種の図形の上の動きが、単純な動きと同じ形に直せるかを問う数学の予想です。1995年にフランスの数学者エティエンヌ・ギスが提起しました。²⁴

論文は、そのうち複素3次元の場合を証明しました。一般の場合は未解決です。²

作業	AIがしたこと	人がしたこと
証明を作る	8月から様々な方向を試し、数千ページの導出を書き出した⁵	研究チームが全体の方向を決め、有望な筋を選び、AIに指摘を返し続けた⁴⁵
論文にする	アイデアと論証を、複数回の対話で練るのを助けた²	著者が論証を全部自分で確かめ、論文の責任を負った²
Leanの形にする	AIエージェントのSHEAFが、証明をLeanの形に書き起こした²⁶	北京大学のチームが行い、最後の定理は人が確かめた²

論証を確かめて責任を負ったのは、著者です。²

論文と報道から分かるGhys予想の証明の流れ。人が方向を決めてAIと何度も対話し、完成した証明は別のチームがLeanで検証しました。査読を受けたという記述は見つかりませんでした。

Leanは、証明の一歩一歩を計算機が検査する、数学用のソフトです。北京大学のチームが、論文の主な定理をLeanの言葉に置き換え（形式化し）ました。作業にはAIエージェントのSHEAFを使っています。²⁶ コードは公開されています。³

公開されたコードでは、4つの定理が、未証明を示す記号sorryなしで証明されています。³

ただし、そのうち3つは、別の数学者が過去に示したとコードの説明にある結果を、正しいものとして使っています。この結果は、このコードの中では確かめていません。³

論文が査読を受けたという記述は、読んだ範囲では見つかりませんでした。検証をしたのは、著者とは別のチームです。²⁴

この事例から、AIに任せるときの確認点が3つ挙げられます。

たとえばAIに月次の集計表を作らせるなら、元の帳簿と合計が合うかを確かめる人と手順を、先に決めておくということです。

AIの成果は、確かめ方と責任者が決まってはじめて、ほかの仕事の土台にできると考えています。

まずは、いまAIに任せている長い作業を1つ選び、結果をどう確かめるかを書き出してみてください。