HEXAGONbeta

A Lean formalization of Waldschmidt's subgroup theorem with period term for groups with elliptic factors

Primarily AI-generated textHuman understanding: no partsmath.NT — Number Theory

Contributed by Shawn Krisman ↗

Version 1 / Nov 07, 2026 / CC BY 4.0

Abstract

We formalize in Lean 4 with Mathlib Waldschmidt's algebraic subgroup theorem with period term (Theorem 4.1 of his 1988 Durham paper) for G=Gad0×Gmd1×E1×⋯×EmG=\mathbb{G}_{\mathrm{a}}^{d_0}\times\mathbb{G}_{\mathrm{m}}^{d_1}\times E_1\times\dots\times E_m, with EjE_j elliptic curves with algebraic invariants, under the additional hypothesis 2N≥d1+2d0+κ2N\ge d_1+2d_0+\kappa. The proof uses only Lean's three standard axioms. Along the way we give what we believe are the first formal proofs of Schneider's theorems on elliptic functions and of the Schneider--Lang criterion, and the first Lean library for the Weierstrass σ\sigma and ζ\zeta functions. Restricted forms of the theorem cover some vector extensions and the Jacobian of y5=x(1−x)y^5=x(1-x). A companion certificate uses these to prove explicit cases of the four exponentials conjecture: for example, 2ϖ2^{\varpi} and 3ϖ3^{\varpi} are not both algebraic, where ϖ\varpi is the real period of y2=4x3−4xy^2=4x^3-4x, and likewise 2B(1/5,1/5)2^{B(1/5,1/5)} and 3B(1/5,1/5)3^{B(1/5,1/5)}.

Provenance statement

The research, paper and lean certificate were all done by Claude Opus 5.5

Tools used

Anthropic
Claude OpusVersion 5.5

References

  1. W. Bosma; H. W. Lenstra. Complete systems of two addition laws for elliptic curves. J. Number Theory, vol. 53, pp. 229–240. 1995
  2. G. V. Chudnovsky; D. V. Chudnovsky. Irrationality exponents of real CM elliptic periods and powers of the lemniscate period. 2026. with Lean files. arXiv:2610.31112
  3. L. de Moura; S. Ullrich. The Lean 4 theorem prover and programming language. Automated Deduction – CADE 28, vol. 12699, pp. 625–635. 2021
  4. M. Eberl; W. Li; L. C. Paulson. From Weierstraß to Dedekind via Jacobi: formalising foundations of modular forms. 17th International Conference on Interactive Theorem Proving (ITP 2026), vol. 382, pp. 23:1–23:19. 2026
  5. M. Karatarakis; F. Wiedijk. A formalization of the Gelfond–Schneider theorem. 2026. arXiv:2603.24823
  6. Shawn Krisman. A Lean formalization of Roy's strong six exponentials theorem. 2026. preprint
  7. Shawn Krisman. A proof of the Roy–Waldschmidt theorem with period term, with explicit consequences at CM and Beta periods. 2026. unrefereed draft, in the \leanpaper/ folder of \citeLeanMstar
  8. Shawn Krisman. four-exponentials-cm-periods. 2026. called \leanlean_mstar in this paper; library \leanCM4E, with this project as a Lake dependency. https://github.com/telaviv/four-exponentials-cm-periodslink
  9. Shawn Krisman. strong-six-exponentials. 2026. https://github.com/telaviv/strong-six-exponentialslink
  10. Shawn Krisman. waldschmidt-subgroup-theorem. 2026. https://github.com/telaviv/waldschmidt-subgroup-theoremlink
Show all 24 referencesShow fewer references
  1. S. Lang. Introduction to Transcendental Numbers. Addison-Wesley. 1966
  2. M. Laurent. Indépendance linéaire de valeurs de fonctions doublement quasi-périodiques. C. R. Acad. Sci. Paris Sér. A, vol. 290, pp. 397–399. 1980
  3. D. W. Masser. Elliptic Functions and Transcendence. Springer, vol. 437. 1975
  4. C. Perassi. diaz-modulus-lean: Transcendence theory in Lean 4. 2026. accessed October 2026. https://github.com/carlok/diaz-modulus-leanlink
  5. P. Philippon. Lemmes de zéros dans les groupes algébriques commutatifs. Bull. Soc. Math. France, vol. 114, pp. 355–383. 1986. Errata et addenda, ibid. 115 (1987), 397–398
  6. D. Roy. Matrices whose coefficients are linear forms in logarithms. J. Number Theory, vol. 41, pp. 22–47. 1992
  7. D. Roy; M. Waldschmidt. Autour du théorème du sous-groupe algébrique. Canad. Math. Bull., vol. 36, pp. 358–367. 1993
  8. Th. Schneider. Arithmetische Untersuchungen elliptischer Integrale. Math. Ann., vol. 113, pp. 1–13. 1937
  9. The mathlib Community. The Lean mathematical library. Proceedings of CPP 2020, pp. 367–381. 2020
  10. M. Waldschmidt. Sous-groupes analytiques de groupes algébriques. Ann. of Math. (2), vol. 117, pp. 627–657. 1983
  11. M. Waldschmidt. On the transcendence methods of Gel'fond and Schneider in several variables. New Advances in Transcendence Theory (Durham, 1986), pp. 375–398. 1988
  12. M. Waldschmidt. Linear independence of logarithms of algebraic numbers. 1992. revised 2016. IMSc Report 116, Madras
  13. M. Waldschmidt. Diophantine Approximation on Linear Algebraic Groups. Springer, vol. 326. 2000. Chapters 5 and 8 by D. Roy
  14. G. Wüstholz. Algebraische Punkte auf analytischen Untergruppen algebraischer Gruppen. Ann. of Math. (2), vol. 129, pp. 501–517. 1989

Version history

  1. v1 · 30 pagesSubmitted by Shawn KrismanInitial depositCurrentNov 06, 2026