AxiomMath/Stacks

选用指南

AI 根据 README 整理 · 2026/11/5 12:46:38

适用场景

适合需要验证代数几何定理证明、或参与形式化贡献的研究人员。

查看 README 依据

references](#ega-and-sga-references)). Examples, exercises and remarks that are not yet formalized are left as tasks for contributors (see §[Contributing](#contributing)). Lean's kernel checks every proof. There is no `sorry` and no `native_decide`. ## Structure `import Stacks` brings in both tiers. Every proof in either tier is kernel-checked; the tiers differ in who has reviewed the code. * [StacksCore](StacksCore/): human-reviewed formalizations, checked against the Stacks Project and brought to Mathlib standards of naming, generality and style.

`lake exe cache get` downloads Mathlib's compiled files. The library itself has about 63,000 modules, so a full build takes a long time and a lot of memory; a cache service for the compiled Stacks modules is planned, so that `lake build` will not have to compile them locally. ## Contributing Contributions are welcome: formalizing the remaining examples, exercises and remarks, reviewing StacksFrontier code and moving it into StacksCore, formalizing directly for StacksCore, or improving existing proofs.

使用方式

通过Lean 4和Lake进行构建和使用，导入Stacks后可使用#stacks_tags命令列出全部带标签的声明。

查看 README 依据

Stacks`, the command `#stacks_tags` lists every tagged declaration with its tag, and `#stacks_tags!` also prints each statement. The [website](https://stacks.axiommath.ai/) links each tag to its Lean code, its dependencies and the Stacks Project's own statement. ## EGA and SGA references

* a special case of the item: the restriction, for example `"affine case"`. A declaration that is only related to an item, without proving any of these, is not tagged with it. Numbers follow the original installments: Publ. Math. IHÉS for EGA, and the standard Springer Lecture Notes editions for SGA. ## Axioms Proofs use only the standard axioms `propext`, `Classical.choice` and `Quot.sound`. After `import Stacks`, `#print axioms` on any declaration lists exactly what it rests on. ## Building ``` lake exe cache get lake build ```

部署要求

需要Lean 4 (v4.34.0-rc2)和Mathlib，完整构建耗时且占内存，约63,000个模块。

查看 README 依据

[](https://axiommath.ai/) # The Stacks Project in Lean * [Website](https://stacks.axiommath.ai/) A Lean 4 (v4.34.0-rc2) formalization of [the Stacks Project](https://stacks.math.columbia.edu/), the open-source reference work on algebraic geometry, built on [Mathlib](https://github.com/leanprover-community/mathlib4). We have formalized every tag of the Stacks Project with formalizable content, and declarations are also tagged with the items of Grothendieck's *Éléments de géométrie algébrique* (EGA) and *Séminaire de géométrie algébrique* (SGA) that they prove (see §[EGA and SGA

`lake exe cache get` downloads Mathlib's compiled files. The library itself has about 63,000 modules, so a full build takes a long time and a lot of memory; a cache service for the compiled Stacks modules is planned, so that `lake build` will not have to compile them locally. ## Contributing Contributions are welcome: formalizing the remaining examples, exercises and remarks, reviewing StacksFrontier code and moving it into StacksCore, formalizing directly for StacksCore, or improving existing proofs.

已知限制

StacksFrontier中的形式化由AI代理编写，需要人工审查后才能移入StacksCore；未形式化的例子、练习和评注留作贡献者任务。

查看 README 依据

references](#ega-and-sga-references)). Examples, exercises and remarks that are not yet formalized are left as tasks for contributors (see §[Contributing](#contributing)). Lean's kernel checks every proof. There is no `sorry` and no `native_decide`. ## Structure `import Stacks` brings in both tiers. Every proof in either tier is kernel-checked; the tiers differ in who has reviewed the code. * [StacksCore](StacksCore/): human-reviewed formalizations, checked against the Stacks Project and brought to Mathlib standards of naming, generality and style.

* [StacksFrontier](StacksFrontier/): formalizations written by AI agents. This is where coverage grows fastest, and where review is most needed before code moves into StacksCore. ## Finding a tag A declaration that formalizes all or part of a Stacks tag carries the attribute `@[stacks TAG]`, for example `@[stacks 00DS]`; a tag that Mathlib already covers is registered on the Mathlib declaration with `add_to_stacks TAG`. A tag can be carried by several declarations, and a comment in the attribute records which part of the tag a declaration covers when it covers only part. After `import