Axiom Math、数学からAIスロップを遠ざける取り組みを発表

Axiom Mathは、人間が書いた最大級の数学文献の一つであるStacks Projectを形式検証したと発表した。同社のAIエージェントが約7,654ページの内容を約1,600万行のLeanコードに変換し、コンピュータによる検証を行った。Stacks Projectは2005年にJohan de Jongがオープンソースの参照資料として始めたもので、代数幾何を含む分野をカバーする。同社は3月に2億ドルのシリーズAを調達し、Menlo Venturesが主導した。