Formalizing Extended Complex Numbers, Mobius Transformations, and Cross Ratio in Lean 4
Fubin Yan, Kenneth W. Shum
math.CV
Jun 18, 2026 · v3
cs.MS
TL;DR
Formalizes the extended complex plane as Option ℂ, Möbius transformations, and cross-ratio invariance in about 6,000 lines of Lean 4 using Mathlib.
Abstract
The extended complex plane is a fundamental object in complex analysis, hyperbolic geometry, and mathematical physics. Its geometry is governed by Möbius transformations, with the cross ratio serving as a central invariant. We present a formalization of these concepts in the Lean4 theorem prover. The extended complex plane is represented using Mathlib's Option type over $\mathbb{C}$, where the additional element represents the point at infinity. On this foundation, we define Möbius transformations, their action on the extended complex plane, and the cross ratio. We formalize several basic properties of Möbius transformations, including their group structure, and identify them with a projective general linear group. We also prove the uniqueness of a Möbius transformation mapping any three distinct points to any other three distinct points, and the invariance of the cross ratio. All proofs are machine-checked in Lean 4. The complete development comprises approximately 6,000 lines of Lean code, including about 40 definitions and 150 lemmas and theorems. This work provides a verified foundation for future formalizations of conformal geometry, hyperbolic models, modular forms, and applications in mathematical physics.
Problem
Mathlib develops complex analysis on the ordinary complex plane but has no formalization of the Riemann sphere, Möbius transformations, or the cross ratio. These are basic objects for conformal geometry, hyperbolic models, and modular forms.
Approach
The extended complex plane is defined as Option ℂ, with none standing for the point at infinity, and arithmetic is defined by pattern matching. Möbius transformations are a structure holding four coefficients and a proof that the determinant is nonzero, with an action defined by case analysis on the pole and on infinity. The cross ratio is defined by pattern matching on which arguments are infinite. Proofs rely heavily on field_simp, ring, and norm_cast, with explicit case splits for the infinite cases.
Results
The formalization proves the group structure of Möbius transformations and their identification with PGL(2,ℂ). It also proves that a transformation fixing three distinct points is the identity, gives existence and uniqueness of the transformation sending three distinct points to three others, and proves invariance of the cross ratio. A realization of S4 as a subgroup is included. The development has about 40 definitions and 150 lemmas, and the code is on GitHub.
