AxiomがStacks Project全編をLeanで形式化、1600万行の数学ライブラリが誕生

The Stacks Project, Formalized in Lean

Axiomが、代数幾何学の基盤となる約7500ページのStacks Project全体をLeanで形式化し、1600万行規模の再利用可能な数学ライブラリとして公開した。Johan de Jongが2005年に始めた恒久的なタグ構造をそのまま保持し、各Lean宣言を原典に対応付けて閲覧できる。形式化の過程では、仮定の欠落や標数正のedge caseなど、原典の数十箇所の記述に修正が必要なことも判明した。