Anthropicが8月10日、未公開の研究版Claudeが数学の未解決問題のまわりで下限を一つ動かしたと発表した。リーマン予想そのものは解けていない。動いたのは「ゼータ関数の零点のうち、どれだけが臨界線上にあると証明できるか」という割合で、41.6%から67.2%になった。ただ、暮らしの側から見て効くのは記録の更新ではなく、その証明の正しさを機械が確かめられる形で一緒に公開されたことのほうだ。
進んだのは、予想そのものではない
語の範囲を絞っておきたい。リーマン予想は「ゼータ関数の自明でない零点はすべて臨界線上にある」という主張で、1859年から未解決のままだ。今回動いたのは「すべて」ではなく「少なくともどれだけか」という下限にあたる。従来の記録はPrattらが2020年に示した5/12（約41.66%）で、これが67.25%まで上がった。追加の仮定を置かない、無条件の結果として示されている。
組み立てたのは公開されていない研究版のClaudeだ。Anthropicの説明によれば、2回に分けた作業で650個のアイデアを潰し、約60個のサブエージェントを動かして2,400回のシェルコマンドを走らせ、出力は3,100万トークンに達した。人間が継続的に入れたのは、数学者ではないスタッフによる「続けて」という趣旨の励ましが中心だったと書かれている。
そしてAnthropic自身が、この手法がリーマン予想の証明につながるとは考えていないと明記している。三分の二を超えても、残りは残る。
「専門家にしか確かめられない」が、少し崩れる
35ページの解析的整数論の論文を読んで正しさを判断できる人は多くない。これまで、こういう結果を前にした専門外の人間にできることは、権威を信じるか判断を保留するかの二択に近かった。
今回はそこに三つ目が置かれている。定理はLean 4という証明支援系で形式化され、GitHubで公開されている。リポジトリの説明によれば、主要な定理AからEまでがsorry（証明を書かずに開けておく穴）なしで通っており、Leanの標準の三つの公理以外に前提を置いていない。論証に使う解析的な道具——明示公式や零点の個数の評価など——も外からの引用ではなく、中で証明されている。
確かめる手順も書かれている。elanを入れ、lake exe cache getでビルド済みのMathlibを取得し、lake buildを通す。エラーもsorry警告も出なければ、その証明はLeanのカーネルが通したということになる。
関係が裏返っている。信じるか保留するかではなく、走らせるかどうかになった。
ただし、確かめられるのは「どこまで」か
手放しでは書けない部分を並べておく。
機械が通したのは「論証に穴がないこと」であって、「その定理が何を意味するか」ではない。67.2%が数学として何の位置にあるのかは、依然として読み手の理解の側に残る。ビルドが緑になっても、分かったことにはならない。
Leanの外にも前提が一つ残っている。リポジトリの説明では、PairCeilingと呼ばれる部分だけが256個の整数区間に値が収まることを仮定していて、その確認はLeanの中ではなく外部の区間演算で行われている。証拠となる有理数の証明書はハッシュで固定されているものの、入手は著者への請求という形だ。ただしこの仮定が効いているのは補助的な結果に限られ、67.2%を含む主定理はこの仮定に依存しないとリポジトリは明記している。それでも、リポジトリ全体が公開ビルドだけで端から端まで閉じるわけではない。
手間もかかる。Leanの環境を入れ、指定のバージョンに揃え、大きなライブラリを取得してからでないと始まらない。プログラミングの経験がまったくない状態で最初に触るものとしては軽くない。
人間の目も抜けていない。Anthropicの数学者2人が内容を確認し、この分野の専門家であるBrian ConreyとDan Goldstonが論文を見ている。一方で、学術誌の査読を経た発表ではなく、Anthropic自身のサイトからの公開だ。
自分は、何をもって「確かめた」ことにするのか
これは数学の話に見えて、判断の手続きの話でもある。AIが出してきた結論を前に、自分は何をもって納得するのか。
選べる道は増えた。誰が言ったかで決める。専門家のレビューを信じる。自分で走らせて、機械が通ったことを確認する。あるいは通したうえで、外に残った前提まで読みにいく。どれを選ぶかで、かかる手間も、分かる範囲も変わる。
形式化されたコードが付いてくる主張は、これからも例外のままだろう。多くの場面では、手元で走らせる選択肢がそもそも無い。だからこそ、手段が用意されている事例は、無い場合との差がどこにあるのかを測る物差しになる。
あなたは、AIが出した答えのどこまでを、自分の手で確かめておきたいだろうか？
