TY - RPRT TI - Formalization of Sullivan's No Wandering Domains Theorem in Lean AU - Ziang Li AU - Yusheng Luo PY - 2026 UR - https://arxiv.org/abs/2609.16027 ID - 2609.16027 ER -