AI生成の数学論文5本が受理！00後創業者・洪楽潼が14億ドル調達
Axiom Math社（創業者は00後中国系の洪楽潼）が、AIシステムAxiomProverが生成した8本の数学論文のうち5本が査読付きジャーナルに受理されたと発表。同社は3月に20億ドルの資金調達を完了し、評価額160億ドルに達した。
記事インテリジェンス
要点
- Axiom MathのAIシステムAxiomProverが生成した8本の数学論文のうち5本が学術誌に受理された。
- 創業者・洪楽潼はスタンフォード大学を中退して起業し、20億ドルを調達、評価額160億ドル。
- AxiomProverは「生成＋形式証明＋検証」のパイプラインで数学的正当性を保証する。
- 同社は自己改善型の超知能推論器の開発を目指し、すでにゲーム理論の定理も形式証明した。
重要な理由
このニュースが重要なのは、Axiom MathのAIシステムAxiomProverが生成した8本の数学論文のうち5本が学術誌に受理されたためです。
技術的影響
モデル選定、推論コスト、プロダクト能力、評価基準に影響する可能性があります。
Axiom Math社（本社未公表）は2026年5月28日、同社のAIシステム「AxiomProver」が生成または形式証明した8本の数学論文のうち、5本が査読付き学術誌に受理されたと発表した。創設者は2001年生まれの中国系天才数学者・洪楽潼（ホン・ラトン）氏である。
受理された論文は、数論、組合せ論、可換代数、代数幾何学、表現論、Dyck pathモデルなど多岐にわたる。特に「Reciprocals of Partition Polynomials」と題された論文は、ルーマニア科学アカデミー紀要に受理され、Ballantine、Beck、Feigon、Maurischat氏らが提起した10個の予想のうち6個を解決し、さらに1つの反例を発見した。
AxiomProverの特徴は、自然言語による証明ではなく、形式証明アシスタント「Lean」を用いて証明を生成する点にある。別の検証器が証明の各ステップを自動チェックし、人間の数学者が形式証明を学術的な解説文に変換する。この協業により、AIは与えられた未解決問題に対して約24時間で完全な機械検証済み証明を生成できるという。
洪氏は幼少期から数学の才能を示し、14歳で「MIT」と書いたノートを励みに、華南師範大学附属高校からMITに進学。3年で数学と物理学の二重学士号を取得し、ローズ奨学金とモーガン賞（北米数学本科生最高栄誉）を受賞。オックスフォード大学で神経科学修士号を取得後、スタンフォード大学の数学・法学博士課程に進むが、2024年秋に中退してAxiom Mathを創業した。共同創業者Shubho Sengupta氏（元Meta）とともに、AIの幻覚問題を解決すべくスタートした。著名数学者Ken Ono氏もバージニア大学の終身教授職を辞して参加。
同社はシードラウンドで6400万ドル、シリーズAで2億ドル（約13.56億元）を調達し、評価額は160億ドル（約108.46億元）に急成長。投資家Matt Kraning氏は「AIはすべてのコードを書くだろうが、数学はそれが正しいかどうかを証明する」と評した。
Axiom Mathの最終目標は、自己改善型の超知能推論器の開発。5月27日に提出された最新論文はゲーム理論と経済学に跨り、ハーバード・ビジネススクール教授Scott Duke Kominers氏と共同でRobert Aumannの古典的定理をLeanで形式証明した。洪氏は「起業家は最も難しい問題を選ぶべき。解決に5～10年かかってもよい」と語っており、彼女の選択した道は、AI業界でも最も注目される分野の一つとなっている。