2026年10月7日の朝、「OpenAI、社内AIがリーマン予想の関連難問を証明と主張」という見出しが並びました。GitHubに置かれた原稿は722本で、リーマン予想、ホッジ予想、BSD予想と、教科書でしか見かけない名前が続きます。

数学は、もう人間の手を離れてしまったのか。見出しだけを追えば、そう感じるのも自然です。

しかし722本の中身を開くと、景色が変わります。AIの原稿がいちばん多く引いている人間は、スーツケース一つで世界を回り、賞金つきの宿題を配り歩いた数学者エルデシュでした。別の原稿は、43年前にグロタンディークが手紙に書き残した予想に挑み、その中核に京都の研究者たちが30年かけて磨いた道具を据えています。

「AIが人間を置き去りにした」と片づけるには、この話は少し面白すぎます。

OpenAI数学722本 Executive Summary（情報図解）

10月7日にGitHubへ722本の原稿が置かれた

OpenAIは日本時間10月7日の早朝、GitHubに「openai/math」というリポジトリを公開しました。中身は、社内の未公開モデルが生成したとする数学の原稿722本です。関連する原稿は372の「結果ファミリー」に束ねられ、著者欄はどれも「OpenAI」です。

READMEによれば、評価の期間中にモデルへ約4,000問が出題され、大半の結果は同じ手順で得られました。1件あたりの計算は、平均でChatGPT Proの思考およそ3時間分です。ただし準リーマン予想とホッジ予想（CM）の仕事は、この固定手順の「例外」とされています。

数字は、それぞれ数えているものが違います。約4,000は出題した問題の数、372は束の数、722は原稿の数です。722を4,000で割っても、出てくるのは「正答率」とは別の数です。

「722本」は何の数か

READMEは、最初からこう断っています。

"Some of the unformalized results could have issues. We will endeavor to fix any such issues quickly." （形式化されていない結果の中には、問題を含むものがあるかもしれない。そうした問題は速やかに修正するよう努める。）

「証明した」と「確かめられた」のあいだ

722本は、どれもOpenAIが「証明した」と主張している原稿です。それが数学の知識として受け入れられるまでには、少なくとも三つの段階があります。

  • 主張：論文を書き、公開した段階。722本はすべてここにいます
  • 機械の検査：証明をLean（リーン）という言語に書き直し、コンピューターに一行ずつ論理を確かめさせた段階
  • 人間の確認：専門家が論文を読み込み、正しいと公に認めた段階

Leanは強力な検査役です。「ここは明らか」という省略も、権威ある学術誌への信頼も通用しません。

ただし、Leanが保証するのは「形式化された主張」とその証明が噛み合っていることまでです。書き直した主張が数学者の言う予想と本当に同じか、論文の残りの部分が正しいかは、守備範囲の外にあります。準リーマン予想のLeanを手元で再ビルドした利用者も、「これが確かめたのはLeanの証明で、論文ではない」と書き添えています。

シリーズで取り上げた8つの主張を、この物差しで並べると次のようになります。

8本の主張は、どこまで確かめられているか

半分の4つはLeanの検査が主定理や予想そのものに及び、残りの4つは論文の証明だけで公開されています。そして10月7日の時点で、8つのどれについても、専門家が論文を読み通して正しいと公に認めた例は、確認できた範囲ではゼロでした。

人間の証明も確かめるのに年単位かかってきた

時間がかかるのは、書いたのがAIだからではありません。人間の書いた証明も、確定までに長い時間と他人の目を必要としてきました。

「解いた」から「確かめられた」までの時間

いちばん痛い例は、このシリーズの中にあります。1954年、ザランキェヴィチはトゥランのレンガ工場問題を証明したとする論文を、権威ある学術誌に載せました。帰納法の穴が見つかったのは11年後で、その間、証明は定理として扱われていました。

1976年の4色定理は、計算機に頼った証明が「本当に証明と呼べるのか」という議論を呼び、2005年に証明支援系Coqでの形式証明が完成しました。1998年に発表されたケプラー予想の証明は、査読者が何年かけても「99%確か」としか言えず、形式証明の完了は2014年です。

確かめる側の主役は、いまも人間です。ミレニアム懸賞を運営するクレイ数学研究所も、適格な媒体での発表から少なくとも2年がたち、世界の数学界で一般に受け入れられていることを、授賞の条件にしています。

AIの原稿は人間の肩の上に立っている

722本の参考文献欄をすべて数えると、AIの原稿がだれの仕事の上に立っているかが見えてきます。OpenAI自身の原稿への引用を除いた、人間の文献だけの集計です。

AIの原稿は、だれの仕事を引いているか

引いている結果ファミリーの数で数えると、最も多いのはポール・エルデシュで、372のうち41ファミリーでした。没後30年の数学者が世界中に残した問題と論文が、AIの「部品棚」のいちばん手前に並んでいます。

日本の研究者では森重文氏（14ファミリー）が最も多く、京都大学（数理解析研究所を含む）ゆかりの研究者を引くファミリーは、筆者が所属を手作業で振り分けた概算で、372のうち60前後ありました。個人を超えて最も多く引かれていたのは、世界中の研究者が共同で書き継ぐオンライン教科書「Stacks Project」（53ファミリー）です。ただし「いちばん引かれた人」は、数え方で入れ替わります。

「いちばん引かれた数学者」は、数え方で変わる

参考文献の件数で数えると、1位は京都大学の藤野修教授（極小モデル理論）で、120件にのぼります。その多くは互いに関連する少数の原稿グループに集中しており、引いているファミリーの数で数え直すと12です。どの順位も誤りではなく、何を数えたかの違いです。

ここに、AIの仕事の意外な人間くささがあります。AIが多くの結果を出した分野には、人間が厚く積み上げてきた道具箱がありました。極小モデル理論の一群では藤野氏の定理群が標準の部品になり、遠アーベル幾何学の原稿では、望月新一氏と辻村昇太氏の定理が中核に据えられています。

AIの原稿は、AI自身の過去の成果の上にも積み上がっています。OpenAIの原稿どうしの引用は596件あり、BSD予想をめぐる論文も、まだだれも確かめていない自社の論文を土台にしています。

8つの問いに、人間がかけてきた時間

8つの問いが生まれてから今年まで、合わせて約700年です。AIが主張する答えは、その700年分の問いの立て方と道具の上に書かれています。

解くことは目的なのか

公開の約4週間前の9月11日、フィールズ賞受賞者たちが「A Severe Misalignment of AI in Mathematics（数学におけるAIの深刻な目標の乖離）」という宣言を公表しました。署名欄には、森重文、ドリーニュ、ショルツェ、テレンス・タオら28名が並びます。公式の日本語版には、次の一文があります。

「しかし、問題を解くことは、概念的な理解と洞察という第一の目標を達成するための道具であり、間接的な指標にすぎません。」

解くこと自体が偉いのではなく、解く過程で数学の理解、ひいては世界の理解が深まることに意味がある、という考え方です。エルデシュ問題のサイトを運営する数学者トーマス・ブルーム氏も、公開と同じ10月6日（米国時間）に「未解決」「解決済み」の表示をやめ、解決の件数も出さないことにしました。

この視点は大切です。答えだけが届き、だれも中身を説明できないなら、それはまだ数学の一部になる手前にあります。しかし、結論が出ること自体にも、やはり価値があります。

  • 仮定や「どこからかは言えない」が外れる：数論には、リーマン予想を仮定した定理や、例外の零点のせいで定数を具体的に計算できない定理が数多くあり、準リーマン予想の主張が正しければ、その一部から仮定や不自由さが外れます。数論研究者を名乗るHacker Newsの投稿者は、この結果を使えば自分の2018年の論文が3ページ短くなると書き、「こういう論文はおそらく何百本もある」と続けました。
  • 反例が、間違った方向の掘削を止める：722本には、予想を覆す反例もあります。No.196は、1940年のヒグマンの博士論文にさかのぼり、1956年にカプランスキーが問題として掲げた「零因子予想」に、反例を作ったと主張しています。反例の構成はLeanで形式化されており、主張が正しければ「成り立つはず」と信じて掘り続ける道は、そこで終わります。
  • 確定した結論は、次の土台になる：4色定理もケプラー予想も、計算機に頼った証明のあり方には議論が残りました。それでも結論が確定したことで、後に続く人はその上に安心して積み上げられるようになりました。

理解が深まることに、意味がある。そのうえで、結論が出ることそのものにも、確かな価値があります。

はじめての方へ：8本の歩き方

8つの問いには、それぞれ一本ずつ記事を書きました。どこから読んでも完結しますが、数式が苦手な方には、絵で追える問いから入る順番をおすすめします。

はじめての方へ：8本を読む順番の一例

1. 方眼紙の上の飛び石：ガウス素数の堀

方眼紙の交点に散らばる「素数の石」だけを踏んで、決まった歩幅のまま、どこまでも遠くへ行けるか。1962年に投げかけられたこの問いに、No.028は「行けない、どこから出発しても、たどれる島の大きさに上限がある」と答えたと主張しています。Leanの検査は主定理まで及んでいます。

計算機が掘り当てた堀の記録や、「平面なら回り道できそう」という素朴な直感と専門家の直感のずれを、実データの図でたどれます。最初の一本に向いています。

記事を読む →

2. 強制労働の工場で生まれた問い：トゥランのレンガ工場

1944年、強制労働に駆り出された数学者トゥランは、台車がレールの交差で脱線するたびに「交差は最少で何か所まで減らせるのか」と考えました。82年後、No.165はこの問題と兄弟分のヒルの予想を両方とも解いたと主張し、Leanの形式証明も付けています。一度は「解けた」とされた証明が11年後に崩れた歴史が、この記事の柱です。

「3軒の家と電気・ガス・水道」のパズルから入れます。「描ける」と「それ以下は無理」の違いは、会議室でもそのまま使える物差しです。

記事を読む →

3. 針を一回転させる最小の広さ：掛谷問題

1917年、東北帝国大学の掛谷宗一が問うた「長さ1の針を回すのに要る最小の面積」は、「いくらでも小さくできる」という奇妙な答えのあと、「次元」の問いに生まれ変わりました。2025年に人間が3次元を解いてフィールズ賞につながり、No.074は4次元を証明したと主張しています。Leanは付いておらず、検証はこれからです。

日本人の名を冠した問いの110年を、図形の図で追えます。物差しを替えると、同じものが正反対の顔を見せます。

記事を読む →

4. だれに払うのか分からない5,000ドル：エルデシュ

エルデシュが「払うことになるとは思っていない」と書いた等差数列の予想に、No.159は証明を主張し、予想そのものはLeanの検査を通っています。しかし賞金の規程が求めるのは査読付き専門誌への掲載で、AIや会社が受け取る場合の定めはありません。

1年前の「10問解いた」騒動との対比も読みどころです。「本当に未解決だったか」「機械はどこまで確かめたか」「だれが認めたか」という三つの問いは、社内のAI活用報告にもそのまま当てはまります。

記事を読む →

5. 「解いた」を見極める6つの問い：BSD予想

「OpenAIがBSD予想を解いた」という噂は、公開前に予測市場の値まで動かしました。実際に公開されたNo.002は、ランク1までの楕円曲線について精密な公式を主張する論文で、ミレニアム懸賞の問いとは範囲が違います。Leanは付かず、土台にはまだ確かめられていない自社の論文があります。

「どこまで解いたのか」「だれが確かめたのか」など6つの問いは、仕事に届く「業界初」「精度99%」のニュースにも使えます。

記事を読む →

6. 167年の山の中腹に打たれた杭：準リーマン予想

リーマン予想そのものは、いまも未解決です。No.003は、ゼータ関数の零点が実部7/8より右には現れないと主張し、主定理は標準の定義のままLeanの検査を通りました。応用部分と約200ページの論文本体を人間が確かめるのは、これからです。

「今は何合目なのか」という素朴な疑問に、素数の数え間違いの桁で答えます。

記事を読む →

7. 粘土の模様をLEGOで組めるか：ホッジ予想（CM）

ホッジ予想は「図形の穴の模様（粘土の作品）を、方程式で描いたブロック（LEGO）で組み直せるか」を問う予想です。No.032は、数十年前から「ここさえ証明できれば」と名指しされてきた「CMアーベル多様体」という箱の中で、それを証明したと主張しています。Leanは付いておらず、外部の専門家による確認の公表は、まだこれからです。

ポアンカレの『位置解析』からペレルマンまで、130年の物語として読めます。

記事を読む →

8. 1983年の手紙と京都の道具箱：グロタンディーク×望月

グロタンディークが1983年の手紙に書き残した「切断予想」の局所版について、No.019は証明したと主張しています。その幾何の中核には、望月新一氏と辻村昇太氏が2023年に発表した定理が、名指しで組み込まれていました。Leanは付いておらず、正しいかどうかは遠アーベル幾何学の専門家の目にかかっています。

ABC予想の論争とは別の、望月氏のもう一つの顔に出会えます。AIと形式化について望月氏自身が書いてきた言葉も紹介しています。

記事を読む →

「AIが解いた」と聞いたら

8本を通して浮かぶのは、次の三つの問いです。

  • どこまで：見出しの「解いた」と、論文が主張する範囲は同じか
  • 機械はどこまで：Leanなどの検査は、主張のどの部分に及んでいるか
  • だれが：発表した本人以外の専門家は、確かめたか

同じことは、数学の外でも言えます。AIが書いた報告書や企画書を受け取ったときも、同じ三つを問うだけで、「すごい」と「怪しい」のあいだにある正確な大きさが見えてきます。

AIは722本の原稿を書きました。しかしその原稿は、エルデシュの宿題、グロタンディークの手紙、京都の道具箱、掛谷の針の上に書かれています。答えが正しいかを最後に確かめるのも、人間です。

「人間はもうついていけない」で片づけるには、もったいない話です。700年分の問いが答えの形になって、いま人間の手に戻ってきました。

参考文献