Axiom 将 Stacks Project 全量转为 Lean 形式化代码

Everyone assumes AI-written code at scale means a giant pile of slop. Me too at times. Axiom just put out the best counterexample I've seen. They took the Stacks Project, the reference every algebraic geometer works from, built up by the math community over two decades, and turned the whole thing into Lean. Millions of lines, and every single one is checked by a computer. It either holds up or it doesn't compile. What gets me isn't even the size, it's the structure. Stacks is this massive web where every result leans on a bunch of others. Axiom compares it to the glass pyramid at the Louvre, all these individual pieces that only make sense once you see how they fit together. They kept all of that intact, just in a form a machine can check. They ran their agents like a software team to do it, with some owning the architecture, some the core definitions, some the individual proofs, and humans at the top. To be clear, the math is still human work. People wrote Stacks. What's new is that i

来源：X · Linus Ekenstam · x.com