AIと数学

国際数学オリンピック。世界中の高校生の天才が、2日間で、6問に挑みます。1日に3問、4時間半。

2024年、ここにAIが挑戦しました。結果は、42点満点の、28点。金メダルの基準は、29点。あと、1点。

しかも、問題によっては、3日かけていました。制限時間とは、何だったのでしょう。

数学の証明は、答えが合えばいい、という世界ではありません。最初の1行から最後の1行まで、全部が正しくないと、0点です。

もっともらしい文章が得意なAIには、最悪の相性。「たぶん合ってます」が、通用しないのです。

そこで使われたのが、Leanという、証明専用の言語。証明をプログラムのように書くと、コンピュータが1行ずつ、正しいかを判定します。

いわば、絶対に見逃さず、部分点もくれない、世界一厳しい採点者。AIは、この先生に数えきれないほどバツをもらって、証明の書き方を覚えました。

そして2025年。Google DeepMindのAIは、人間と同じ問題文を読み、同じ4時間半で、6問中5問を正解。35点。金メダルの水準です。

3日が、4時間半に。たった1年の出来事です。

ただ、オリンピックは、答えのある問題です。では、まだ誰も答えを知らない問題は、どうでしょう。

4行4列の行列どうしを掛けるのに、掛け算は何回要るか。1969年から、最高記録は49回でした。2025年、AIが見つけた手順は、48回。

56年ぶりの更新が、たったの1回ぶん。地味に見えますか。この1回のために、半世紀かかったんです。

ただし、派手なニュースには、注意が要ります。2025年、「AIが未解決問題を10問解いた」という発表がありました。

調べてみると、答えは、昔の論文にすでに載っていました。AIがやったのは、証明ではなく、世界一優秀な、文献検索。…それはそれで、すごいのですが。

数学者テレンス・タオの見立てでは、ある有名な未解決問題集のうち、いまのAIがほぼ自力で解けるのは、易しい1〜2%ほど。

長年解かれていない問題には、本当に難しいものと、誰も本気を出していなかっただけのものが、あるのです。

それでも、AIが証明を書き、機械が検証する時代は、もう始まっています。数学者の仕事は、解くことから、どの問題に価値があるかを、見抜くことへ。

…このセリフ、AI科学者の回でも言いました。どうやら、どの分野でも、人間に残る仕事は同じようです。