SHEAF 公开 Lean 4 形式化工作流与证明项目

SHEAF 公开 Lean 4 形式化工作流与证明项目 工具以依赖图、目标锁定、依赖裁剪及 Lean 检查协调 Agent 的形式化工作，相关 HolomorphicAnosov 项目提供了证明代码和构建检查命令。

证明范围与前提需按论文和仓库审阅，项目仍依赖一个尚未在该库证明的经典拓扑结果假设，不应扩张为 AI 独立证明了所有相关猜想。