使用 Lean 4 与 mathlib 逐步形式化环面几何，将格、锥与扇等组合基础连接到分裂环面射影丛、轨道分层、扇细分、爆破和初等变换；以经典例子校验数学约定，并建立可编译、可复用的机器检查证明。

2026-10-20

lean-toric

lean-toric 是一个使用 Lean 4 与 mathlib 形式化环面几何的项目，目标是把分裂环面向量丛及其射影化中的组合结构，逐步转化为可编译、可复用的机器检查证明。

项目研究扇与格、分裂射影丛、坐标子丛和轨道分层，并延伸到扇的星细分、环面爆破、压缩及初等变换。当前已建立格、锥和扇的 Lean 基础设施，并完成射影空间扇的形式化；围绕后续定理，也整理了明确的数学约定、例子和证明路线。项目从组合基础出发，为复杂几何构造建立逐层验证的形式化框架。

项目强调数学表述与形式化实现同步推进：固定关键符号和约定，用具体的经典例子检查构造，并以无占位证明、完整编译作为正式验收标准。其阶段化设计也为将来连接代数几何对象、Cox 环与 GIT 理论留下了清晰接口。