Lean

約1万5000ページの巨大な数学証明を機械検査　AxiomがLean形式化コードを公開

Axiomは2026年10月26日付の公式発表で、数学の「有限単純群の分類」について、初の完全なコンピューター検査可能な証明を公開したと発表した。同社によると、人間が指揮する数十のAIエージェントを使い、24日間で約4310万行のLeanコードを作成した。