Axiom Math、数学書庫をLeanで形式検証

AI数学スタートアップのAxiom Mathは、人間が作成した大規模な数学資料「Stacks Project」を形式検証したと発表しました。約7654ページの内容を、コンピューターで検査できる約1600万行のコードに変換しました。

Stacks Projectは2005年に始まったオープンソースの数学リファレンスで、代数学や幾何学、数論などを扱います。AxiomのAIエージェント群が資料の形式化に取り組みました。

形式検証では、証明をLeanという言語のコードに書き換え、証明支援プログラムが行ごとに論理の整合性を確認します。コードが検査を通れば、証明の論理的な正しさを確かめる仕組みです。

同社は、検証済みの数学基盤をAIエージェントがソフトウェア作成や将来の科学研究に使えるようにする構想です。AIが作る数学的成果への信頼性を高められるかが、今後の焦点になります。