Pith. sign in

REVIEW 2 minor 13 references

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.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · grok-4.3

2026-06-26 15:06 UTC pith:JXNJOEIG

load-bearing objection A straightforward Lean 4 library that machine-checks the standard uniqueness and invariance results for Möbius transformations on the extended plane.

arxiv 2606.20358 v2 pith:JXNJOEIG submitted 2026-06-18 math.CV cs.MS

Formalizing Extended Complex Numbers, Mobius Transformations, and Cross Ratio in Lean 4

Fubin Yan , Kenneth W. Shum This is my paper
classification math.CV cs.MS
keywords Lean 4formalizationMöbius transformationscross ratioextended complex planecomplex analysistheorem proving
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper builds a formalization in Lean 4 of the extended complex plane by representing it as an Option type over the complex numbers, with none standing for the point at infinity. It defines Möbius transformations as maps on this space and identifies them with the projective general linear group. The authors prove that these transformations form a group and that there is a unique one sending any three distinct points to any other three distinct points. They also establish that the cross ratio remains unchanged under the action of any Möbius transformation. All of these statements receive machine-checked proofs in the development of roughly 6000 lines of code.

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.

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.

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.

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.

Watch this falsifier — get emailed when new claim-graph text bears on it.

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.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

0 major / 2 minor

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)
  1. §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.
  2. 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

0 responses · 0 unresolved

We thank the referee for their positive assessment of the manuscript, including the evaluation of its significance and the recommendation to accept.

Circularity Check

0 steps flagged

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.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The development rests on Mathlib's existing formalization of complex numbers and the Option type; no new free parameters, ad-hoc axioms, or invented entities are introduced beyond the standard modeling of infinity.

axioms (1)
  • standard math Mathlib's definitions of ℂ and Option are correct and match the classical mathematical objects.
    The entire formalization is built directly on top of these library primitives.

pith-pipeline@v0.9.1-grok · 5736 in / 1153 out tokens · 27496 ms · 2026-06-26T15:06:54.147898+00:00 · methodology

0 comments
read the original 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.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

13 extracted references · 1 canonical work pages · 1 internal anchor

  1. [1]

    L. V. Ahlfors. Complex analysis -- an introduction to the theory of analytic functions of one complex variable. McGraw-Hill, 3rd edition, 1979

    1979

  2. [2]

    J. W. Brown and R. V. Churchill. Complex variables and applications. McGraw Hill Education, 9th edition, 2014

    2014

  3. [3]

    de Moura and S

    L. de Moura and S. Ullrich. The L ean 4 theorem prover and programming language. In Int. Conf. on Automated Deduction, July 2021

    2021

  4. [4]

    H. M. Farkas and I. Kra. Riemann surfaces, volume 71 of Graduate texts in mathematics. Springer-Verlag, 1980

    1980

  5. [5]

    Progress in Formalizing Sphere Packing in Dimension 8

    S. Hariharan, Christopher Birkbeck, Seewoo Lee, Ho Kiu Gareth Ma, Bhavik Mehta, Auguste Poiroux, and Maryna Viazovska. A milestone in formalization: The sphere packing problem in dimension 8, April 2026. arXiv:2604.23468v2 [math.MG]

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  6. [6]

    Harrison

    J. Harrison. Formalizing basic complex analysis. Studies in Logic, Grammer and Rhetoric, 10 0 (23): 0 151--165, 2007. URL https://github.com/jrh13/hol-light/tree/master/Complex

    2007

  7. [7]

    Harrison

    J. Harrison. Formalizing an analytic proof of the prime number theorem. J. Automatic Reasoning, 43: 0 243--261, 2009

    2009

  8. [8]

    Kontorovich and T

    A. Kontorovich and T. Tao. Prime number theorem and more, January 2024. URL https://github.com/AlexKontorovich/PrimeNumberTheoremAnd

    2024

  9. [9]

    Li and Paulson

    W. Li and Paulson. A formal proof of C auchy’s residue theorem. In 7th Int. Conf. Interactive theorem proving, pages 235--251, 2016

    2016

  10. [10]

    Mari\'c and D

    F. Mari\'c and D. Petrovi\'c. Formalizing complex plane geometry. Annals of Math. and Artificial Intelligence, 74: 0 271--308, 2014. URL https://isa-afp.org/entries/Complex_Geometry.html

    2014

  11. [11]

    Strong PNT , 2025

    Math Inc. Strong PNT , 2025. URL https://math-inc.github.io/strongpnt/

    2025

  12. [12]

    Z. Shi, Y. Guan, and X. Li. Formalization of Complex Analysis and Matrix Theory. Sprigner, 2020

    2020

  13. [13]

    E. M. Stein and R. Shakarchi. Complex analysis. Princeton lectures in analysis II . Princeton Unverstity Press, New York, 2003

    2003