AxiomMath、Stacks Projectを1600万行のLeanコードに形式化

評価額16億ドルのAxiomMathは、Stacks Projectを正式に検証したと発表した。約7654ページの数学文献を、AIエージェントを使ってコンピューターで検査可能な約1600万行のLeanコードに翻訳したもの。チームはエージェントに緩やかな階層を設定し、並列に自らタスクを引き受けさせ、数学を得意とする自社開発モデルを用いた。CEOのCarina Hong氏は、AIエージェントに再利用可能な検証基盤を提供し、低品質な成果物を減らす狙いがあると述べ、同規模の形式化をコーディング企業に公開で挑んだ。