Axiom把七千多页的Stacks Project炼成约1600万行Lean库并开源；人工细审大约只占千分之二。