OpenAI、10件の数学的成果をLeanで形式化——内部モデルが担った役割

8月1日、OpenAIは原稿「Ten Advances in Mathematics and Theoretical Computer Science」を公開し、その成果を自社の内部モデルによるものとした。同時にGitHubリポジトリ `openai/ten-proofs` が作られ、10件の証明のLean 4形式化が公開されている。成果のなかで目を引くのは、球充填の指数の改善——1978年以来はじめてのことだ——、非ソフィック群の構成、そしてコンヌの剛性予想への反例である。リポジトリはmathlibを土台にしたLean 4.32.0のプロジェクトで、ライセンスはApache-2.0。誰でも `lake exe cache get` と `lake build All` で証明を再コンパイルでき、ComparatorChallengesフォルダには独立に検証する手順が説明されている。

報道はこれらの成果を、OpenAIが同じ8月1日に発表した次期モデル群の名前「Astra」と結びつけた。ただし原稿が語るのは「内部モデル」だけで、そのモデルは公開されていない。トークン費用およそ2,000ドルや文書の249ページといった数字は第三者の報道によるもので、公式の告知ページは現在アクセスできない。論文は読み直しをした人間の数学者に謝辞を述べ、Shuoxing Zhou氏による独立かつ同時期の研究にも触れている。その研究は一部、GPT-5.6 Solの助けを借りて進められた。

SiliconANGLEによれば、数学的な議論はモデルから出たものだが、それを公開できる原稿に仕上げたのは人間の研究者だった。その仕上げがどれほどの比重を占めるのかは数値化されていない。Lean 4の採用は論点を移す。証明書は証明の論理的な正しさを保証するが、形式化された命題が歴史的な未解決問題と一致することまでは自動的に保証しない——その確認は人間の仕事のままだ。10件のいずれも正式な査読を通っていない。前例が重くのしかかる。2025年10月、GPT-5がエルデシュの問題を10件「解いた」という発表は根拠を欠くことが判明し、erdosproblems.comを管理するThomas Bloom氏はこれを重大な誤った表現だと述べた。今回の10件について、同じBloom氏は「big news」と語っている。理論物理学者のTobias J. Osborne氏が指摘するように、示された2,000ドルは当たった分のトークンの費用であって、試行全体の「収穫」ではない。その点についてOpenAIは何も明らかにしていない。こうした状況は、2026年6月に公表され、the-decoderによれば3,000人を超える数学者と国際数学連合が支持する「Leiden Declaration on Artificial Intelligence and Mathematics」——透明性、著作者の権利の保護、成果に対する人間の責任を求める文書——を背景としている。

本当のニュースは、機械が数学をしたことではない。それはもう何か月も続いている。今回は成果のひとつひとつに再コンパイル可能なLean証明書が添えられていることだ。判断するのに、発表する側を信用する必要はない。とはいえ、失敗した試行と成功の比率が企業秘密であり続けるかぎり、これらのモデルの効率の評価は統計というより信仰の問題であり続ける。