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 2 / 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. D. Bertrand. La théorie de Baker revisitée. The reference list of \citePW88 gives the title as La méthode de Baker revisitée. Publ.\ Math.\ Univ.\ P. et M. Curie 73, Groupe d'Étude sur les Problèmes Diophantiens 1984–85, no. 2, 25 pp.
  2. W. Bosma; H. W. Lenstra. Complete systems of two addition laws for elliptic curves. J. Number Theory, vol. 53, pp. 229–240. 1995
  3. 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
  4. L. de Moura; S. Ullrich. The Lean 4 theorem prover and programming language. Automated Deduction – CADE 28, vol. 12699, pp. 625–635. 2021
  5. 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
  6. M. Karatarakis; F. Wiedijk. A formalization of the Gelfond–Schneider theorem. 2026. arXiv:2603.24823
  7. S. Krisman. A Lean formalization of Roy's strong six exponentials theorem. 2026. Hexagon preprint 2610.00338v1, https://hexagonmath.org/2610.00338v1hexagon
  8. S. Krisman. A proof of the Roy–Waldschmidt theorem with period term, with explicit consequences at CM and Beta periods. 2026. unrefereed extended draft, in the \leanpaper/ folder of \citeLeanMstar
  9. S. Krisman. Four exponentials at CM and Beta periods. 2026. Hexagon preprint 2611.00171v1, https://hexagonmath.org/2611.00171v1hexagon
  10. S. Krisman. four-exponentials-cm-periods. 2026. library \leanCM4E, with this project as a Lake dependency. https://github.com/telaviv/four-exponentials-cm-periodslink
Show all 27 referencesShow fewer references
  1. S. Krisman. strong-six-exponentials. 2026. https://github.com/telaviv/strong-six-exponentialslink
  2. S. Krisman. waldschmidt-subgroup-theorem. 2026. https://github.com/telaviv/waldschmidt-subgroup-theoremlink
  3. S. Lang. Introduction to Transcendental Numbers. Addison-Wesley. 1966
  4. 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
  5. D. W. Masser. Elliptic Functions and Transcendence. Springer, vol. 437. 1975
  6. C. Perassi. diaz-modulus-lean: Transcendence theory in Lean 4. 2026. accessed October 2026. https://github.com/carlok/diaz-modulus-leanlink
  7. 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
  8. P. Philippon; M. Waldschmidt. Formes linéaires de logarithmes sur les groupes algébriques commutatifs. Illinois J. Math., vol. 32, pp. 281–314. 1988
  9. D. Roy. Matrices whose coefficients are linear forms in logarithms. J. Number Theory, vol. 41, pp. 22–47. 1992
  10. D. Roy; M. Waldschmidt. Autour du théorème du sous-groupe algébrique. Canad. Math. Bull., vol. 36, pp. 358–367. 1993
  11. Th. Schneider. Arithmetische Untersuchungen elliptischer Integrale. Math. Ann., vol. 113, pp. 1–13. 1937
  12. The mathlib Community. The Lean mathematical library. Proceedings of CPP 2020, pp. 367–381. 2020
  13. M. Waldschmidt. Sous-groupes analytiques de groupes algébriques. Ann. of Math. (2), vol. 117, pp. 627–657. 1983
  14. M. Waldschmidt. On the transcendence methods of Gelfond and Schneider in several variables. New Advances in Transcendence Theory (Durham, 1986), pp. 375–398. 1988
  15. M. Waldschmidt. Linear independence of logarithms of algebraic numbers. 1992. revised 2016. IMSc Report 116, Madras
  16. M. Waldschmidt. Diophantine Approximation on Linear Algebraic Groups. Springer, vol. 326. 2000. Chapters 5 and 8 by D. Roy
  17. 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 depositSupersededNov 06, 2026
  2. v2 · 31 pagesSubmitted by Shawn KrismanSubmitted as a new versionSupersededNov 07, 2026
  3. v3 · 31 pagesSubmitted by Shawn KrismanSubmitted as a new versionCurrentNov 10, 2026