Paul Erdős が残した未解決問題を1つずつ番号を付けて管理し、その状態を示してきたウェブサイトが、運営の方針を大きく変えた。問題ごとの『解決』の表示と、解決した問題の数の集計をやめる。誰が解いたかという手柄の記録もやめる。代わりに重んじるのは、人間が読める解説と、証明支援系 Lean で検証された形式的な証明である。変更は、Terence Tao のブログに10月6日付の『Changes to the Erdős problems web site』として載った（一次情報）。
きっかけは、AI が出す証明の急増である。証明は届くが、なぜそれで成り立つのかを説明していない。そうした提出に、サイトは押し流された。『解決』の印を付け、解いた人の名前を並べ、解決数を数え上げる仕組みは、AI が答えを量産する時代には、何も理解されていない問題にまで『済み』の札を貼ってしまう。サイトはこの札そのものを外した。
『正しい答え』は、もう希少ではない
Erdős 問題のサイトは、AI の数学の能力を測るための非公式な物差しとしても使われてきた。問題の数が多く、難しさにも幅がある。しかも1つひとつの問題に、解決済みか未解決かの印が付いている。AI の企業にとっては『何問解いた』と言える格好の材料だった。解決数の集計をやめれば、この物差しは使えなくなる。
背景には、この数週間の出来事がある。OpenAI は9月、社内のモデルがナビエ・ストークス方程式の問題を解き、ほかにも100件を超える長年の未解決問題を片付けたと発表した。166ページの原稿と、コンパイルの通る Lean の形式化も公開されており、技術的には正しいというのが大方の見方である。それでも、クレイ数学研究所はこの問題を未解決の一覧に残したままにしている。
NPR は9月22日に『AI は数学最難問の一つを解いた。人類は（いまのところ）何も学んでいない』と報じた。オックスフォードの James Maynard は『この新しい AI の証明から人間の理解を引き出すのは、これまでのところ非常に難しい』と述べた。ブラウン大学の Javier Gómez-Serrano は『この論文は人間向けに書かれていない』、NYU の Tristan Buckmaster は『ひどい書き方の論文だ』と評している。正しさはもう争点ではない。問われているのは、その正しさから人間が何を得たかである。
正しさは Lean に任せ、人間には理解を求める
今回の変更で目を引くのは、評価の役割を2つに分けたことである。証明が正しいかどうかは、Lean の形式的な検証で機械的に確かめられる。AI の証明を数学者が1行ずつ追って審査する負担を、ここで切り離せる。一方、その結果が数学として何を意味するのかは、人間が読める解説がなければ伝わらない。サイトが重んじる対象を答えから解説へ移したのは、この2つ目こそが、数学者の共同体が本当に積み上げたいものだという判断である。
この考え方は、Tao のブログに9月から続いたゲスト投稿で、繰り返し論じられてきた。Caltech の Tapio Schneider は9月24日の『Headlines and inside stories』で、正しいが理解できない証明は『見出し』を与えるだけで、『内幕の物語』を与えないと書いた。Amit Sahai は、AI の結果を人間が確かめられるよう、数学者をもっと厚く育てるべきだと論じた。Northwestern の Antonio Auffinger は、AI による証明の加速が数学の共有の文化を侵していると警告した。前日の10月5日には、同じブログに『The future of mathematics』が載っている。Erdős 問題のサイトの変更は、こうした議論が、運営の仕組みにまで入り込んだ最初の具体例と言える。
『誰が解いたか』が意味を失う
手柄の記録をやめたことも重い。数学では長く、ある問題を最初に解いた人の名前が成果の単位だった。だが、AI が下書きを出し、人間がそれを整え、別の AI が形式化する、という流れでは、『誰が解いたか』に答えること自体が難しい。10月4日に同じブログに載った Diego Córdoba と Luis Martínez-Zoroa のゲスト投稿は、オイラー方程式とナビエ・ストークス方程式の最近の研究のうち、大規模言語モデルを使ったものをはっきり引いていた。AI による結果は、すでに先行研究として引用される側に入っている。
こうなると、名前の付いた『解決』を数えることは、数学がどれだけ進んだかを測る物差しとしても、人の業績を認める仕組みとしても、うまく働かなくなる。サイトはその両方を降りた。残すのは、問題について人間が何を理解したかの記録である。
数学が『成果』を定義し直し始めた
今回の変更は、1つのサイトの運営方針にとどまらない。数学の共同体が、何を成果と認めるかを、自分たちで定義し直し始めたことを示している。AI の企業は、解いた問題の数を性能の宣伝に使ってきた。フィールズ賞受賞者25人が9月11日に出した公開書簡は、未解決問題を AI のベンチマークの宣伝に使うことを批判していた。数学者の側はこれに対し、数える対象そのものを変えるという手で応じたことになる。
問われる点は残る。Lean の証明と人間向けの解説の両方を、誰がどれだけ書くのか。AI が解説まで書くようになったとき、その解説は『人間が読める理解』に数えてよいのか。人間の理解をどう記録し、評価するのかという運営の具体は、これから試されることになる。それでも方向ははっきりしている。答えが安くなった世界で、数学の共同体は、答えを積み上げることより、理解を積み上げることを選び始めた。
