投稿者: 数学の自動形式化を手がける Math Inc. が開発した AI システム「 Gauss 」が、数学界で大きな話題を呼んでいます。フィールズ賞受賞者らが 18 カ月以上格闘していた「強い素数定理（ Strong Prime Number Theorem ）」の形式化を、わずか 3 週間で完了させたのです。
「強い素数定理」は、素数の分布を記述する古典的な素数定理をより強化したバージョンです。2024 年 1 月、フィールズ賞受賞者のテレンス・タオとアレックス・コントロヴィッチが、この定理を数学証明支援システム「 Lean 」で形式化するプロジェクトを始めました。しかし複素解析の難しい部分で行き詰まり、2025 年 7 月時点でも完成には至っていませんでした。
Gauss は、複雑な数学の定理を機械が読める形式、つまり検証可能な証明コードに自動変換する AI です。これまでトップレベルの専門家でも何年もかかる作業でしたが、Gauss は高い自律性を持ち、膨大な数の定理や定義を短時間で形式化できます。
今回の成果では、約 25,000 行の Lean コードと 1,000 以上の定理・定義を生成しました。数千の AI エージェントが同時に協力し、各エージェントが最大 12 時間働き続けました。人間の専門家は全体設計と重要部分のチェックだけを担当する仕組みが取られています。
技術的には、Lean 証明支援システムと自社開発の大規模分散環境（ Morph Labs Trinity ／ infinibranch ）によって膨大な計算資源を活用しています。これまで未解決だった複素解析の難しい部分、例えば「リーマンゼータ関数の零点非存在領域」なども新たに形式化することに成功しています。
Math Inc. は元 Google の AI 研究者 Christian Szegedy が創業した企業で、「数学を解くことですべてを解く」をモットーとしています。同社は今後 12 カ月で形式化コードの総量を 100 〜 1,000 倍に増やし、「検証済み超知能」の基盤構築を目指すと発表しています。