Sullivan No Wandering Domains theorem 完成 Lean 4 形式化；Claude agents 辅助局部证明与 boilerplate

Ziang Li 与 Yusheng Luo 发布 Sullivan No Wandering Domains theorem 的 Lean 4 形式化：次数至少为 2 的 Riemann sphere 有理自映射，其每个 Fatou component 最终都会周期化。项目同时形式化 normal families、Montel–Carathéodory theorem、Julia/Fatou sets、Sobolev regularity、Cauchy/Beurling transforms、quasiconformal equivalence 与 measurable Riemann mapping theorem 等大量基础。公开仓库说明总体架构和核心 theorem statements 由人类设计与核验，Claude agents 辅助 individual proofs 与 boilerplate；项目无 sorry 或新增 axiom。