math.NT — Number Theory

A lean formalization of Roy's strong six exponentials theorem

Contributed by Shawn Krisman

We formalize in Lean 4 with Mathlib Roy's strong six exponentials theorem: if $x_1,x_2$ are linearly independent over $\overline{\mathbb{Q}}$ and $y_1,y_2,y_3$ are linearly independent over $\overline{\mathbb{Q}}$, then one of the six products $x_iy_j$ lies outside the $\overline{\mathbb{Q}}$-vector space spanned by $1$ 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 $\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 $\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.