REVIEW 2 minor 1 cited by
Formalizing Extended Complex Numbers, Mobius Transformations, and Cross Ratio in Lean 4
T0 review · 0 major / 2 minor · reviewed 2026-06-26 · grok-4.3
Pith's one-line read Möbius transformations mapping any three distinct points to any three others are unique, with the cross ratio invariant under them, all machine-checked in Lean 4.
desk verdict A straightforward Lean 4 library that machine-checks the standard uniqueness and invariance results for Möbius transformations on the extended plane. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
The Option type representation of the extended complex plane, which supports the definition of Möbius transformations and the cross ratio together with their verified algebraic and geometric properties.
What would settle it
A concrete set of three distinct points and three target points for which the Lean formalization either finds more than one Möbius transformation or none at all would falsify the uniqueness claim.
Extended reading notes
Core claim
The extended complex plane is represented using Mathlib's Option type over ℂ. Möbius transformations are defined on this space, shown to form a group identified with PGL(2,ℂ), and proved to act uniquely when mapping any three distinct points to any other three distinct points. The cross ratio is defined and shown to be invariant under these transformations, with every step machine-checked in Lean 4.
Load-bearing premise
Modeling the extended complex plane as Mathlib's Option type over the complex numbers faithfully captures the standard mathematical object along with its topology and geometry.
Editorial extensions
If this is right
- Möbius transformations can be used inside formal proofs of conformal geometry without risk of undetected algebraic mistakes.
- The cross ratio functions as a machine-verified invariant for geometric configurations on the extended plane.
- The library supplies a verified base for formal work on hyperbolic models and modular forms.
- Applications in mathematical physics can draw on these checked geometric facts rather than informal arguments.
Reading between the lines
- The same representation might be reused to formalize additional invariants or fixed-point properties of Möbius transformations that the paper leaves unstated.
- Integration with other Mathlib developments on projective geometry could shorten proofs that combine complex analysis with linear algebra.
- The code base could serve as a test case for measuring how much human effort is saved when later papers build directly on machine-checked libraries.
Signed reviews
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper claims to formalize the extended complex plane via Mathlib's Option ℂ (with none as infinity), Möbius transformations as fractional-linear maps on this space, their group structure and identification with PGL(2,ℂ), the uniqueness of a Möbius transformation sending any three distinct points to any three distinct points, and the invariance of the cross ratio, all with machine-checked Lean 4 proofs comprising ~6000 lines, 40 definitions and 150 lemmas.
Significance. If the modeling is faithful to the classical objects, the work supplies a verified, reusable foundation inside Mathlib for subsequent formalizations of conformal geometry, hyperbolic models, and related topics. The machine-checked status of the uniqueness and invariance theorems, together with the absence of free parameters or ad-hoc axioms, strengthens the reliability of the development.
minor comments (2)
- §3 (Möbius transformations): the notation for the action on Option ℂ could be clarified by explicitly stating the handling of the infinity case in the main definition rather than only in the lemmas.
- The cross-ratio definition in §4 uses a ratio of differences; a brief remark on why this extends continuously at infinity would aid readers unfamiliar with the Option encoding.
Simulated Author's Rebuttal
We thank the referee for their positive assessment of the manuscript, including the evaluation of its significance and the recommendation to accept.
Circularity Check
No significant circularity; machine-checked formalization of standard results
full rationale
The paper defines the extended complex plane via Mathlib's Option ℂ (standard encoding for adjoining infinity) and then proves algebraic properties of Möbius transformations and cross-ratio invariance inside Lean 4. These are standard facts once the action is defined; the proofs are machine-checked against an independently maintained library with no fitted parameters, self-referential definitions, or load-bearing self-citations. The central claims reduce to verified lemmas rather than any of the enumerated circular patterns.
Assumptions & free parameters
assumptions (1)
- standard math Mathlib's definitions of ℂ and Option are correct and match the classical mathematical objects.
Cite this review
Pith. "Pith review of Formalizing Extended Complex Numbers, Mobius Transformations, and Cross Ratio in Lean 4." pith.science (2026). https://pith.science/paper/JXNJOEIG
@misc{pith2026260620358,
author = {Pith},
title = {Pith review of: Formalizing Extended Complex Numbers, Mobius Transformations, and Cross Ratio in Lean 4},
year = {2026},
howpublished = {\url{https://pith.science/paper/JXNJOEIG}},
note = {Machine review of arXiv:2606.20358}
}
abstract
The extended complex plane is a fundamental object in complex analysis, hyperbolic geometry, and mathematical physics. Its geometry is governed by M\"obius 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\"obius transformations, their action on the extended complex plane, and the cross ratio. We formalize several basic properties of M\"obius transformations, including their group structure, and identify them with a projective general linear group. We also prove the uniqueness of a M\"obius 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.
Forward citations
Cited by 1 Pith paper
-
Generation and purification of excited spacetimes using Schwarzian derivative
Constant-Schwarzian ODEs classify conformal maps that create, purify, or preserve thermal left/right fluxes for a 2D massless scalar, recovering Rindler and many siblings.
Reviewed June 26, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.