数学史上最大の定理をLeanで完全形式化、その過程で既発表論文の誤りを発見

Classification of Finite Simple Groups Formalized in Lean

有限単純群の分類は、約100人の数学者が数十年かけて数千ページにわたり築いた巨大な定理だ。これを第一世代の証明に沿ってLeanで完全形式化し、全論理ステップをカーネルで検証した。43.1M行のLeanコード、205万の宣言、715の文献を要する成果で、作業中にはUnbalanced Group Theoremの既発表の議論に問題を発見し、代替の証明経路を示している。