最近、数学界では人工知能の画期的な進展が見られました。元量化研究者であるNeel Somani氏は、GPT5.2モデルをテストしている際に、AIがわずか15分で数学の伝説的数学者ポール・エルデシュ（Paul Erdős）が未解決にした難問の完全な証明を提示したことを発見しました。その証明の厳密さはLeanなどの形式化ツールによって検証されています。

長年、エルデシュが残した1000を超える数学的予想は、人間の知恵の限界とされていました。しかし昨年のクリスマスからこのウェブサイトでは、15の問題が「解決済み」とマークされ、そのうち11の解決策は明らかにAIの関与があります。

ロボットコンテスト 数学の問題解答

Somani氏は、GPT5.2が数学的推論において前例のない熟練度を示していると指摘しました。これは、レジオンの公式などの公理を巧みに使いこなすだけでなく、ハーバード大学の数学者Noam Elkiesの既存研究に基づいて、より完全な解決策を提示したことも含まれます。このような「長い尾部」の数学的難題を一括して解決する能力は、LLMが人間の知識の境界を広げているかどうかという広範な議論を引き起こしています。

フィールズ賞受賞者である陶哲軒氏は、自身のGitHubページ上でこの進展を詳細に統計し、AIが自主的に進展した8つの事例を記録しています。彼は、AIの拡張性により、複雑で単純な「長い尾部」の問題に対して人間よりも優位であると推測しています。

モデル自体の進化に加え、形式化ツール（例えばHarmonic社のAristotle）の導入も非常に重要です。これらのツールは、AIが生成した推論を自動的にコンピュータで検証可能なコードに変換し、検証プロセスを大幅に簡略化します。Harmonicの創業者Tudor Achim氏は、「解いた問題の数よりも、世界的な数学者がAIツールの使用を公に認め始めていること