AIは数学者を時代遅れにしない
メディアはAIが数学者を置き換えると煽るが、AIは数学的証明の正しさを検証できず、人間が正しさの最終的な判断者であり続ける。
近年、メディアは「AIが数学者を時代遅れにする」という話題を頻繁に取り上げ、毎週のように新しい見出しが登場している。例えば、最近「AIが数学をするとき、数学者であることの意味」という記事が話題になった。
他の学問分野と同様、数学界にもゲートキーピング、流行、派閥、ステータスシグナリングが存在する。もしAIによって数学者という職業が消えても、人類にとっての損失にはならないだろう。数学を行う行為自体は(特にアルゴリズム開発などの民間セクターで)続くが、それは「数学者」という正式な肩書きではなく、「数学を行う人々」になるだけだ。
この議論はどちらの立場でも感情的な反応を引き起こす。スポーツチームの応援よりも個人的な問題だ。AI支持者は芸術や創造性の価値を軽視していると非難され、懐疑派は「終末論者」「ルッダイト」「理解力不足」とレッテルを貼られる。
しかし数学者にとって良いニュースは、AIは時代遅れにはならないということだ。誇大広告で見落とされているのは、AIは証明が正しいかどうかを判断できないという点だ。AIはもっともらしい証明を生成できるが、微妙だが致命的な誤りが含まれていたり、根拠のない仮定をしていることがある。
実際にClaudeやChatGPTで試すことができる。私はClaudeに証明を書かせ、GPTに入力したところ、誤りや論理的欠陥を指摘された。GPTに要約を書かせてClaudeに渡し、修正を加えさせた。このプロセスを少なくとも6回繰り返したが、どちらも相手が納得する証明を最終的に示すことはできなかった。これは最も単純な問題や概念を除いて当てはまる。
実験科学とは異なり、数学では正しさが絶対条件である。少なくとも、証明可能な真理と単なる予想を区別することが重要だ。実験科学は誤りに対して寛容で、試行をやり直せる。AI生成コンテンツが悪い場合も、それは主観的な問題であり、定量的ではない。「数学者は自分の誤りを公表できない」と言われる通りだ。
結局のところ、正しさの判断は人間に委ねられる。数学者がプロンプトを作成し、別の数学者が結果を解釈・チェックする。LEANのようなツールでも、数学者がコードを書き、出力を評価する必要がある。LEANの証明は非常に複雑で冗長であり、困難な結果には数千行のコードが必要で、限られた数学問題にしか対応できない。
また、これらのプログラムは高価でプロプライエタリであり、一般の人が使う商用AIとは異なる。オリンピックやパットナム問題を解くだけでも、かなりのプロンプトと試行錯誤、そして結果が正しいかどうかを検証する人間の多大な作業が必要だ。見出しを飾るエルデシュ問題の背後には、多くの失敗例と、結果を得るための無数のプロンプト作業やトークン消費、そしてそれを検証するための多くの工数が存在する。