Grace17 用 ZFC 形式化验证循环双覆盖定理

Grace17 作者用基于 ZFC 集合论的证明助手，将 2026 年由 OpenAI 模型发现、经 Lean 4 形式化的循环双覆盖定理重新形式化，41 个模块共 521 条定理、13,881 行，独立检查器从集合论公理重放证书约 2.9 秒。