AIが読めない証明を書き、数学者が読める証明を書き直した

AIが数学の難問に挑んで失敗した。ここまでなら珍しい話ではありません。今回おもしろいのは、その失敗の記録を読んだ人間の数学者が、AIとは別の道筋で同じ結果にたどり着き、さらにその先まで進んだことです。

先に断っておくと、このブログの記事はClaudeを使って書いています。今回の主役もClaudeなので、身内の話を身内が書いている形になります。ただし、数学に挑んだのは一般には公開されていない研究用のバージョンで、記事を書いている公開版とは別物です。そのつもりで読んでください。

無理な注文から始まった挑戦

2026年7月末、AnthropicのスタッフJarred Sumnerが、Claudeにひとつ注文を出しました。リーマン予想に本気で挑んでみろ、というものです。本人は数学者ではなく、方針はすべてClaudeに任せたそうです。

リーマン予想は1859年にドイツの数学者リーマンが立てた予想で、素数がどう散らばっているかの秘密を握っています。クレイ数学研究所が100万ドルの懸賞金をかけた7つの問題のひとつでもあり、167年間だれも証明できていません。これを証明しろというのは、どう考えても無理な注文です。

Claudeはまず650通りのアイデアを出して、片っ端から試しました。全部失敗。8月に入って再開するとき、Sumnerは「自分の能力を信じて大きく飛べ」と励ましたのですが、Claudeの返事は「信じ込めば直る類いの問題ではない」という素っ気ないものでした。

それでも作業は続き、Claudeは約60体のサブエージェントを動かして、1日半かけて分担作業をします。既知の零点（ゼロてん）に対する数値チェックを何千回も走らせ、互いの結果を査読し合い、arXivから54本の論文を落として「同じ結果がすでにあるのではないか」まで調べました。2つのセッションで使った出力は合計3,100万トークンです。

リーマン予想そのものは、結局証明できませんでした。

目標を下げたら数字が動いた

証明が無理なら、もっと手前の目標に切り替える。これは数学者が普通にやることです。今回の手前の目標は「零点のうち、どれだけの割合が臨界線（りんかいせん）の上にあると証明できるか」でした。

リーマン予想は「ゼータ関数の零点はすべて1本の縦線の上に並ぶ」という主張です。その縦線を臨界線と呼びます。全部が線上にあるとは証明できなくても、「少なくとも何%は線上にある」なら証明できる。この割合を少しずつ上げていくのが、1世紀以上続いてきた地道な競争でした。

1914年にハーディが「無限個は線上にある」と示し、1942年にセルバーグが「ゼロでない割合がある」と示し、1974年にレヴィンソンが3分の1を超え、1989年にコンリーが5分の2、つまり40%を超えました。そこからは本当に動かなくて、2020年にようやく41.6%。31年かけて1.6ポイントです。

Claudeが出した数字は67.25%でした。しかも「線上にあるだけ」ではなく「線上にあって、なおかつ重なっていない零点」の割合として、です。これを証明した論文は、Anthropic社内の数学者であるLevent AlpögeとRalph Furmanが読んで検証し、外部からもBrian ConreyとDan Goldstonという、この分野の専門家2人が短い期間で目を通しています。あわせて、Leanという証明支援システムで機械的に検証できる形式証明も用意されました。

ただし、これはリーマン予想の証明に近づいたという話ではありません。Anthropic自身が「この手法でリーマン予想が証明できるとは思っていない」とはっきり書いています。仮に99.99%が線上にあると示せても、残り0.01%に例外があれば予想は偽です。割合をいくら上げても、予想の証明にはならない構造になっています。

オックスフォード大学のJames Maynard（2022年フィールズ賞）も、Live Scienceの取材に対して、驚いたのは見出しになる割合の数字ではなく、Claudeの証明に問題と直接かみ合う新しいアイデアが含まれていた点だと話しています。

読むのを諦めた数学者が、元の論文に戻った

ここからが本題です。

フランスのロレーヌ大学で解析数論を研究するYouness Lamzouriは、Claudeの論文が出てすぐに読み始めました。そして数時間で読むのをやめています。何かはあるのだが複雑すぎる、人間の書き方ではない、というのが本人の感想です。

Claudeの証明は、ヴェイユのエルミート形式という道具を有限個の試験関数に制限して巨大な行列を作り、そのトレース（対角成分の和）と成分の二乗和を見積もって、行列の階数（ランク）に関する不等式に流し込む、という作りでした。線形代数の部品がいくつも組み合わさっていて、どこが効いているのかが見えにくい。

そこでLamzouriは、Claudeの論文を追うのをやめて、別のことをしました。Anthropicが「Claudeはこれらの論文に大きく依拠した」と挙げていた既存の論文を、自分で全部読み直したのです。Aryan、それからBaluyot・Goldston・Suriajaya・Turnage-Butterbaughの一連の研究で、モンゴメリーが1973年に（リーマン予想を仮定したうえで）作った「零点の対相関」の理論を、仮定なしで使えるようにしたものです。

読み直しているうちに、Claudeが気づかなかったことに気づきました。巨大な行列を組む必要はなく、ヒルベルト空間の不等式を1本置けば、その先は対相関の定理をそのまま当てはめられる。回り道を全部省いた、ずっと見通しのよい筋道です。

この新しい証明で出てくる数字は、Claudeとまったく同じ67.25%でした。2つの証明は形こそ違いますが、最後はどちらも「零点に関するある二次形式を評価する」問題に帰着し、同じ最適化問題（モンゴメリー＝テイラーの極値問題）に行き着く。だから同じ定数が出る、と論文に書かれています。

Lamzouri本人は、Live Scienceの取材でこの経験を発掘になぞらえています。宝物を掘り出すだけなら重機を入れればいい。でも人間は、なぜそこにそれが埋まっていたのかを知りたいから、手で慎重に掘る。Claudeと自分の間で起きたのはそういうことだ、と。

簡単にしたら、新しいことまで証明できた

見通しがよくなると、同じ道具から別の不等式も引き出せます。Lamzouriの論文には、Claudeの論文には書かれていなかった結果が2つ追加されています。

ひとつは「零点のうち、重なっていないか、臨界線上にあるか、少なくともどちらか一方を満たすもの」が88.76%以上あること。裏返せば、「臨界線から外れていて、しかも重なっている」という、リーマン予想の立場から見て一番たちの悪い零点は、全体の11.2%を超えません。もうひとつは、「重なっていない零点の割合」と「臨界線上の零点の割合」の平均が83.62%以上であること。どちらかが下限の67.25%まで落ちるなら、もう一方は100%に向かわざるを得ない、という硬さを表しています。

この新しい証明にも、Axiom Mathという会社のAIシステムがLeanの形式証明を付けました。Lamzouriの論文は完成直後に、Ken Onoたちのチームが短期間で対応したそうです。人間が見通しのよい証明を書き、AIがそれを機械検証用に書き直す。関係がもう一周しています。

Maynardは、Lamzouriの議論はこの分野の人にとって概念的にずっと明快な組み直しであり、AIがある時代に数学が進んでいくひとつのよい例だと評価しています。Lamzouri自身も、Claudeに触発されたこの見方から、関連する領域で試したいアイデアがいくつも生まれたと話しています。

失敗の記録が手がかりになる

AIと数学の話は、「AIが解いた」か「解いていない」かの二択で語られがちです。今回の筋はそのどちらでもありません。AIはリーマン予想に失敗し、手前の目標で数字を動かし、その証明は人間には読みにくかった。けれど、どの論文を組み合わせたかという記録は残っていて、人間がそれを自分の手でたどり直したら、より単純な証明と、AIが出していなかった新しい事実が出てきた。

同じ月にOpenAIがナビエ＝ストークス問題の証明を発表したときは、人間の数学者が中身を理解できるのか、そこから何か学べるのかが問題になりました。クレイ研究所がミレニアム問題を設定した狙いは、答えを得ることだけでなく、解く過程で新しい手法や理解が生まれることにあります。その意味で、人間に読めない正しい証明より、人間を次の一歩へ押し出した失敗のほうが、数学にとっては価値があったのかもしれません。

注意点もいくつか書いておきます。Claudeの論文も、AlpögeとFurmanによる専門家向けのまとめも、Lamzouriの論文も、いずれも査読前の段階です。Claude側の結果は社内の数学者と外部専門家の検証、Lamzouri側は複数の数論研究者による草稿のチェックとLean形式証明を経ていますが、学術誌への掲載はこれからです。それと、冒頭に書いたとおり、この記事はClaudeで書いています。Claudeを持ち上げる方向に筆が寄っていないか、読む側でも割り引いてもらえると助かります。