数学学術界は最近、技術的な地震を起こした。新興のAI企業アキオム・マスが発表したところによると、同社が自社開発したAIシステムが今年2月から提出した8本の数学論文のうち、5本が正式に査読を通って学術雑誌に掲載されることになった。この突破は、人工知能が純粋数学研究分野において持つ大きな潜在力を示すだけでなく、高難度の複雑な学術的仮説を解決するという点で実質的な一歩を踏み出したことを意味している。

この受け入れられた論文の中には、分割多項式の逆数和（Reciprocals of Partition Polynomials）に関する研究成果が特に注目されている。この研究は長年学界で存在していた10の主要な仮説に直接対応し、AIシステムはそのうち6つを成功裏に証明し、さらに元の命題の中に一つの反例も見つけた。従来のモデルが自然言語を使って「ありそうもない」証明を作成するだけだったのとは異なり、このチームが開発したアキオムプローバー（AxiomProver）システムは新たなワークフローを開拓した。それは、自然言語で表現された数学的問題をLean形式化証明に正確に翻訳し、独立した検出器によってすべての論理ステップを厳密に検証することである。このような「機械による証明、機械による検証、人間の数学者による解釈と補足」という人機協働のモデルにより、AIの「論理的幻覚」は根本的に排除された。

この硬質な科学技術成果の背後にある人物は、わずか25歳の中国の女性である。アキオム・マスの創業者である洪楽潼（ホン・レートン）は、2001年に広州で生まれ、幼少期から驚くべき数学の才能を見せた。彼女は17歳でマサチューセッツ工科大学（MIT）に入学し、3年間で数学と物理の二つの学位を取得し、学部在籍中に9本の論文を発表した。オックスフォード大学の修士号とスタンフォード大学の法学および数学の両方の博士課程への進学資格を獲得した後、彼女は2024年の秋学期にスタンフォードを退学し、起業に専念することを決意した。

洪楽潼の硬派なバックグラウンドと検証可能なAIの壮大なビジョンは、優れた人材と資金の大量流入を引き起こした。Meta AIの元エキスパートであるシュブホ・センゲプタと有名な数学者ケン・オノ（小野健）が相次いで起業パートナーとして加わった。後者は、バージニア大学の終身教職を辞めてまで参加した。一年未満の間に、アキオム・マスは2回にわたる合計2億6400万ドル（約14億元人民元）の資金調達を完了し、会社の評価額はいっきに16億ドルに跳ね上がった。

現在の情報によると、アキオムプローバーは以前からプットナム数学コンテストで満点を取り、数十年にわたるエルデシュ（Erdős）の2つの仮説を解きほぐしたことがある。しかし、洪楽潼とチームの野望は「AI数学者」にとどまらない。最新の研究はゲーム理論と経済学の分野に横断的に進んでいる。このチームは、この「生成・形式化・検証」の閉ループ推論能力を、他の高リスク・高精度要件を持つ意思決定場面にも広げ、自己改善可能なスーパーインテリジェントな推論器の構築を目指している。