HEXAGONbeta

A lean formalization of Roy's strong six exponentials theorem

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

Contributed by Shawn Krisman ↗

Version 1 / Oct 18, 2026 / CC BY 4.0

Abstract

We formalize in Lean 4 with Mathlib Roy's strong six exponentials theorem: if x1,x2x_1,x_2 are linearly independent over Q‾\overline{\mathbb{Q}} and y1,y2,y3y_1,y_2,y_3 are linearly independent over Q‾\overline{\mathbb{Q}}, then one of the six products xiyjx_iy_j lies outside the Q‾\overline{\mathbb{Q}}-vector space spanned by 11 and the logarithms of algebraic numbers. The proof closure uses only Lean's three standard axioms. Along the way the development proves Waldschmidt's transcendence theorem on Gad0×Gmd1\mathbb{G}_a^{d_0}\times\mathbb{G}_m^{d_1} in the form used by Roy, and Philippon's multiplicity estimate with derivatives on Gad0×Gmd1\mathbb{G}_a^{d_0}\times\mathbb{G}_m^{d_1} over every algebraically closed field of characteristic zero, following Roy's account in Waldschmidt's book. We reproduce the public Lean statements, summarize the mathematical route, and record how the artifact is verified. The code is available at https://github.com/telaviv/strong-six-exponentials.

Provenance statement

This was done through a single session with claude code.

Tools used

Anthropic
Claude OpusVersion 5.5

References

  1. de Moura, Leonardo; Ullrich, Sebastian. The Lean 4 Theorem Prover and Programming Language. Automated Deduction – CADE 28, vol. 12699, pp. 625–635. 2021
  2. Guan, Nailin; Hu, Yongle. Formalization of Auslander–Buchsbaum–Serre criterion in Lean4. 2025. arXiv:2510.24818
  3. Karatarakis, Michail; Wiedijk, Freek. A formalization of the Gelfond–Schneider theorem. 2026. arXiv:2603.24823
  4. Lang, Serge. Introduction to Transcendental Numbers. Addison-Wesley. 1966
  5. Laurent, Michel. Linear forms in two logarithms and interpolation determinants. Acta Arith., vol. 66, no. 2, pp. 181–199. 1994
  6. Matsumura, Hideyuki. Commutative Ring Theory. Cambridge Univ. Press, vol. 8. 1986. Translated from the Japanese by M. Reid
  7. Perassi, Carlo. diaz-modulus-lean: Transcendence theory in Lean 4. 2026. Accessed October 2026. https://github.com/carlok/diaz-modulus-leanlink
  8. Philippon, Patrice. 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
  9. Ramachandra, K. Contributions to the theory of transcendental numbers. I, II. Acta Arith., vol. 14, pp. 65–72, 73–88. 1967/68
  10. Roy, Damien. Matrices whose coefficients are linear forms in logarithms. J. Number Theory, vol. 41, pp. 22–47. 1992
Show all 15 referencesShow fewer references
  1. The mathlib Community. The Lean Mathematical Library. Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), pp. 367–381. 2020
  2. Waldschmidt, Michel. On the transcendence methods of Gel'fond and Schneider in several variables. New Advances in Transcendence Theory (Durham, 1986), pp. 375–398. 1988
  3. Waldschmidt, Michel. Linear independence of logarithms of algebraic numbers. 1992. With an appendix by Michel Laurent. Revised version (2016) on the author's web page; chapter numbers refer to it. IMSc Report 116, The Institute of Mathematical Sciences, Madras
  4. Waldschmidt, Michel. Diophantine Approximation on Linear Algebraic Groups. Springer-Verlag, vol. 326. 2000. Chapters 5 and 8 by Damien Roy
  5. Wüstholz, Gisbert. Multiplicity estimates on group varieties. Ann. of Math. (2), vol. 129, no. 3, pp. 471–500. 1989

Version history

  1. v1Submitted by Shawn KrismanInitial depositCurrentOct 18, 2026