TY - RPRT TI - Formalizing Extended Complex Numbers, Mobius Transformations, and Cross Ratio in Lean 4 AU - Fubin Yan AU - Kenneth W. Shum PY - 2026 UR - https://arxiv.org/abs/2606.20358 ID - 2606.20358 ER -