A lean formalization of Roy's strong six exponentials theorem
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/hexagon/2610.00338
curl -X POST /api/v1/records/hexagon/2610.00338/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/hexagon/2610.00338/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'