Stacks Project 代数几何全书完成 Lean 形式化并提供依赖图

Stacks Project 代数几何全书已被系统形式化为 Lean 证明，所有已完成证明均通过 Lean kernel 验证。每条定义、引理、命题和定理保留稳定四字符 tag，可跳转至对应代码及依赖，并通过绿色、红色标签区分已纳入 Mathlib 和不适用于 Lean 形式化的内容。