HEXAGONbeta

Products of pp-adic logarithms of algebraic numbers that are not linear forms in logarithms, and a machine-checked pp-adic linear-subgroup theorem

Primarily AI-generated textHuman understanding: no partsmath.NT — Number Theorycs.LO — Logic in Computer Science

Contributed by Shawn Krisman ↗

Version 1 / Oct 20, 2026 / CC BY 4.0

Abstract

Let pp be a prime, Cp\mathbb{C}_p the completion of an algebraic closure of Qp\mathbb{Q}_p, Q‾\overline{\mathbb{Q}} the algebraic numbers in Cp\mathbb{C}_p, LL the Q\mathbb{Q}-vector space of pp-adic logarithms of algebraic numbers, and L=Q‾+Q‾L\mathcal{L}=\overline{\mathbb{Q}}+\overline{\mathbb{Q}}L the space of pp-adic linear forms in logarithms of algebraic numbers with algebraic coefficients. We prove, in Lean 4 with Mathlib and from the three standard axioms only, that log⁡p2⋅log⁡p(3+2)∉L\log_p 2\cdot\log_p(3+\sqrt2)\notin\mathcal{L} for every prime p≡±3(mod8)p\equiv\pm3 \pmod 8, together with a family of similar statements for real quadratic fields, and the general principle behind them: if σ\sigma is a continuous automorphism of Cp\mathbb{C}_p fixing a nonzero t∈Lt\in L and moving u∈Lu\in L to a conjugate σu≠±u\sigma u\neq\pm u of finite orbit, then tu∉Ltu\notin\mathcal{L}. This is G. Diaz's use of complex conjugation with an element of Gal(Q‾p/Qp)\mathrm{Gal}(\overline{\mathbb{Q}}_p/\mathbb{Q}_p) in its place; the complex analogue log⁡2⋅log⁡(3+2)∉L\log 2\cdot\log(3+\sqrt2)\notin\mathcal{L} is open. The deep input is Roy's form of Waldschmidt's linear-subgroup theorem for Gad0×Gmd1\mathbb{G}_a^{d_0}\times\mathbb{G}_m^{d_1} over Cp\mathbb{C}_p, with a derivative subspace, which we also prove in Lean, from Philippon's multiplicity estimate; the strong six exponentials theorem and the inhomogeneous Baker--Brumer theorem in two logarithms over Cp\mathbb{C}_p follow. The pp-adic linear-subgroup theorem has been used since Laurent and Roy, but we were unable to locate a proof written for Cp\mathbb{C}_p of the version with derivatives. The Lean development is the proof of record; the paper explains the statements, the route, and how to check the certificate. The code is available at https://github.com/telaviv/p-adic-log-products.

Provenance statement

This was done with a single session of Claude Code Fable

Tools used

Anthropic
Claude FableVersion 5.1

References

  1. Bernard, Sophie. Formalization of the Lindemann–Weierstrass theorem. Interactive Theorem Proving (ITP 2017), vol. 10499, pp. 65–80. 2017
  2. Betina, Adel; Dimitrov, Mladen. Geometry of the eigencurve at CM points and trivial zeros of Katz pp-adic LL-functions. Adv. Math., vol. 384, pp. 107724. 2021
  3. Brumer, Armand. On the units of algebraic number fields. Mathematika, vol. 14, pp. 121–124. 1967
  4. Calegari, Frank; Mazur, Barry. Nearly ordinary Galois deformations over arbitrary number fields. J. Inst. Math. Jussieu, vol. 8, pp. 99–177. 2009
  5. Dasgupta, Samit. Ranks of matrices of logarithms of algebraic numbers I: the theorems of Baker and Waldschmidt–Masser. Essent. Number Theory, vol. 2, pp. 93–138. 2023
  6. Dasgupta, Samit; Kakde, Mahesh. Ranks of matrices of logarithms of algebraic numbers II: the matrix coefficient conjecture. Adv. Math., vol. 487, pp. 110753. 2026
  7. de Moura, Leonardo; Ullrich, Sebastian. The Lean 4 Theorem Prover and Programming Language. Automated Deduction – CADE 28, vol. 12699, pp. 625–635. 2021
  8. Diaz, Guy. Utilisation de la conjugaison complexe dans l'étude de la transcendance de valeurs de la fonction exponentielle usuelle. J. Théor. Nombres Bordeaux, vol. 16, pp. 535–553. 2004
  9. Diaz, Guy. Produits et quotients de combinaisons linéaires de logarithmes de nombres algébriques: conjectures et résultats partiels. J. Théor. Nombres Bordeaux, vol. 19, pp. 373–391. 2007
  10. Eberl, Manuel. The Hermite–Lindemann–Weierstraß transcendence theorem. 2021. Archive of Formal Proofs, https://isa-afp.org/entries/Hermite_Lindemann.htmllink
Show all 35 referencesShow fewer references
  1. Fuchs, Clemens; Pham, Duc Hiep. Commutative algebraic groups and pp-adic linear forms. Acta Arith., vol. 169, pp. 115–147. 2015
  2. Fuchs, Clemens; Pham, Duc Hiep. The pp-adic analytic subgroup theorem revisited. pp-Adic Numbers Ultrametric Anal. Appl., vol. 7, pp. 143–156. 2015
  3. Jaulent, Jean-François. Classes logarithmiques des corps totalement réels. Acta Arith., vol. 103, pp. 1–7. 2002
  4. Karatarakis, Michail; Wiedijk, Freek. A formalization of the Gelfond–Schneider theorem. 2026. arXiv:2603.24823
  5. Krisman, Shawn. A Lean formalization of Roy's strong six exponentials theorem. 2026. Preprint and Lean library, https://github.com/telaviv/strong-six-exponentialslink
  6. Krisman, Shawn. p-adic-log-products: Lean 4 proofs of a pp-adic linear-subgroup theorem and of products of pp-adic logarithms outside the linear forms in logarithms. 2026. https://github.com/telaviv/p-adic-log-productslink
  7. Laurent, Michel. Rang pp-adique d'unités et action de groupes. J. Reine Angew. Math., vol. 399, pp. 81–108. 1989
  8. Laurent, Michel. Linear forms in two logarithms and interpolation determinants. Acta Arith., vol. 66, no. 2, pp. 181–199. 1994
  9. Maksoud, Alexandre. On the rank of Leopoldt's and Gross's regulator maps. Doc. Math., vol. 28, pp. 1441–1471. 2023
  10. Matev, Tzanko. The pp-adic analytic subgroup theorem and applications. 2010. arXiv:1010.3156
  11. Momot, Aleksander. Density of rational points on commutative group varieties and small transcendence degree. 2010. arXiv:1011.3368
  12. Perassi, Carlo. diaz-modulus-lean: Transcendence theory in Lean 4. 2026. Accessed October 2026. https://github.com/carlok/diaz-modulus-leanlink
  13. 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
  14. Robert, Alain M. A Course in pp-adic Analysis. Springer-Verlag, vol. 198. 2000
  15. Roy, Damien. Matrices whose coefficients are linear forms in logarithms. J. Number Theory, vol. 41, pp. 22–47. 1992
  16. Roy, Damien. On the vv-adic independence of algebraic numbers. Advances in Number Theory (Kingston, 1991), pp. 441–451. 1993
  17. Serre, Jean-Pierre. Dépendance d'exponentielles pp-adiques. Séminaire Delange-Pisot-Poitou. Théorie des nombres, vol. 7, no. 2. 1965/66. Exp. No. 15, 14 pp.
  18. 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
  19. Waldschmidt, Michel. Transcendance et exponentielles en plusieurs variables. Invent. Math., vol. 63, pp. 97–127. 1981
  20. Waldschmidt, Michel. A lower bound for the pp-adic rank of the units of an algebraic number field. Topics in Classical Number Theory (Budapest, 1981), vol. 34, pp. 1617–1650. 1984
  21. 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
  22. Waldschmidt, Michel. Diophantine Approximation on Linear Algebraic Groups. Springer-Verlag, vol. 326. 2000. Chapters 5 and 8 by Damien Roy
  23. Waldschmidt, Michel. Further variations on the six exponentials theorem. Hardy-Ramanujan J., vol. 28, pp. 1–9. 2005
  24. Waldschmidt, Michel. Variations on the six exponentials theorem. Algebra and Number Theory (Hyderabad, 2003), pp. 338–355. 2005
  25. Waldschmidt, Michel. The four exponentials problem and Schanuel's conjecture. Mathematics Going Forward, vol. 2313, pp. 579–592. 2023

Version history

  1. v1Submitted by Shawn KrismanInitial depositCurrentOct 19, 2026