Motivation

Almost every classical transcendence theorem is a statement about the interaction between the additive structure of $\mathbb{C}$ and the exponential function. Hermite proved in 1873 that $e$ is transcendental, Lindemann in 1882 that $e^{\alpha}$ is transcendental for every nonzero algebraic $\alpha$ — hence that $\pi$ is transcendental and the circle cannot be squared — and Weierstrass in 1885 extended this to the linear independence of $e^{\alpha_1},\dots,e^{\alpha_n}$ over $\overline{\mathbb{Q}}$ for distinct algebraic $\alpha_i$. Gelfond and Schneider settled Hilbert's seventh problem in 1934, and Baker's 1966 theorem on linear forms in logarithms made the subject effective.

Schanuel's conjecture, formulated by Stephen Schanuel in the 1960s and first published by Lang (Introduction to Transcendental Numbers, Addison–Wesley, 1966, Chapter III), is a single statement that contains all of these as special cases, together with a large number of statements that remain open — for instance that $e$ and $\pi$ are algebraically independent, or that $e + \pi$ is irrational. No case of it is known beyond those already covered by the Lindemann–Weierstrass theorem or by Baker's theorem.

Timeline, with the hypotheses each result actually assumes:

• 1882, Lindemann: $e^{\alpha}$ is transcendental for algebraic $\alpha \neq 0$.
• 1885, Weierstrass: for pairwise distinct algebraic $\alpha_1,\dots,\alpha_n$, the values $e^{\alpha_1},\dots,e^{\alpha_n}$ are linearly independent over $\overline{\mathbb{Q}}$.
• 1934, Gelfond and Schneider, independently: if $\lambda \neq 0$ is a logarithm of an algebraic number and $\beta$ is algebraic and irrational, then $e^{\beta\lambda}$ is transcendental.
• 1960s, Siegel, Lang and Ramachandra: the six exponentials theorem, unconditional; the analogous four exponentials statement is still open.
• 1966, Baker: if logarithms $\lambda_1,\dots,\lambda_n$ of algebraic numbers are linearly independent over $\mathbb{Q}$, then $1,\lambda_1,\dots,\lambda_n$ are linearly independent over $\overline{\mathbb{Q}}$.
• 1971, Ax: the function-field analogue of Schanuel's conjecture, for formal power series and, more generally, differential fields of characteristic zero.

Setting

Write $\exp$ for the complex exponential function. A tuple $z_1,\dots,z_n$ of complex numbers is linearly independent over $\mathbb{Q}$ when the only rationals $q_1,\dots,q_n$ with $\sum_i q_i z_i = 0$ are $q_1 = \dots = q_n = 0$; here $\mathbb{C}$ is viewed as a vector space over $\mathbb{Q}$.

For a subset $S \subseteq \mathbb{C}$, let $\mathbb{Q}(S)$ denote the subfield of $\mathbb{C}$ generated by $S$ over $\mathbb{Q}$. The transcendence degree $\operatorname{trdeg}_{\mathbb{Q}} \mathbb{Q}(S)$ is the cardinality of a transcendence basis of $\mathbb{Q}(S)$ over $\mathbb{Q}$: the largest number of elements of $\mathbb{Q}(S)$ that are algebraically independent over $\mathbb{Q}$. A number $x$ is transcendental over $\mathbb{Q}$ when no nonzero polynomial with rational coefficients vanishes at $x$, and numbers $x_1,\dots,x_m$ are algebraically independent over $\mathbb{Q}$ when no nonzero polynomial in $m$ variables with rational coefficients vanishes at $(x_1,\dots,x_m)$.

Formalization targets

Goal

$$z_1,\dots,z_n \text{ linearly independent over } \mathbb{Q} \;\Longrightarrow\; \operatorname{trdeg}_{\mathbb{Q}} \mathbb{Q}\bigl(z_1,\dots,z_n,\,e^{z_1},\dots,e^{z_n}\bigr) \;\ge\; n .$$

The goal fixes no numerical constant and no special shape for the $z_i$: it asserts only the inequality, for every $n$ and every $\mathbb{Q}$-linearly independent tuple. The case $n = 0$ is vacuous and the conclusion is a bound on a cardinal, so nothing is hidden in a degenerate convention.

Milestones

The milestone list consists of the landmark unconditional theorems that Schanuel's conjecture generalizes, the known function-field analogue, and one conditional corollary that records what the conjecture buys:

• Hermite–Lindemann (1882): $\alpha$ algebraic and nonzero $\Rightarrow$ $e^{\alpha}$ transcendental.
• Lindemann–Weierstrass (1885): $\sum_i \beta_i e^{\alpha_i} \neq 0$ for distinct algebraic $\alpha_i$ and algebraic $\beta_i$ not all zero.
• Gelfond–Schneider (1934): $\lambda \neq 0$ a logarithm of an algebraic number, $\beta$ algebraic irrational $\Rightarrow$ $e^{\beta\lambda}$ transcendental.
• Six exponentials theorem: $x_1,x_2$ and $y_1,y_2,y_3$ each $\mathbb{Q}$-linearly independent $\Rightarrow$ at least one of the six numbers $e^{x_i y_j}$ is transcendental.
• Baker (1966): $\mathbb{Q}$-linearly independent logarithms of algebraic numbers, together with $1$, are linearly independent over $\overline{\mathbb{Q}}$.
• Ax (1971), power series form: $\operatorname{trdeg}_{\mathbb{C}} \mathbb{C}(f_1,\dots,f_n,g_1,\dots,g_n) \ge n+1$ when $g_i' = f_i' g_i$, the $g_i$ are units, and no nontrivial $\mathbb{Q}$-linear combination of the $f_i$ is constant.
• Conditional corollary: Schanuel's conjecture implies that $e$ and $\pi$ are algebraically independent over $\mathbb{Q}$.

Significance

Schanuel's conjecture decides, in one stroke, a long list of questions that are individually open: the algebraic independence of $e$ and $\pi$, the irrationality of $e+\pi$ and of $e\pi$, the transcendence of $e^{e}$ and $\pi^{\pi}$, the four exponentials conjecture, and — combined with work of Macintyre and Wilkie — the decidability of the first-order theory of the real exponential field. Its restriction to algebraic $z_i$ is exactly the Lindemann–Weierstrass theorem, and its restriction to $z_i$ whose exponentials are algebraic is exactly Baker's theorem, so the conjecture is a common generalization of the two main unconditional pillars of the subject.

On the formalization side, the state of the art in Lean's mathematical library is modest relative to this history: the analytic core of the Lindemann–Weierstrass argument is present, but the Hermite–Lindemann theorem, the Lindemann–Weierstrass theorem, the transcendence of $\pi$, the Gelfond–Schneider theorem, the six exponentials theorem and Baker's theorem are not available as usable statements in the pinned environment. Each milestone here is therefore a genuine formalization project with a known mathematical proof, and none of them is a restatement of an existing library result. The goal theorem itself is open mathematically; the realistic contributions to it are reductions — implications between the goal and other statements — and closing the milestones that the conjecture generalizes.

Difficulty

The obvious approach to any single case — build an auxiliary function with many zeros, bound its derivatives, and derive a contradiction from an integrality argument — is the method behind every result on the milestone list, and it is exactly what fails for the conjecture in general. Those proofs need the exponentials, or the arguments, to be algebraic somewhere, so that heights and denominators can be controlled; for a general $\mathbb{Q}$-linearly independent tuple there is no arithmetic input at all, and no known construction produces the required auxiliary function. Ax's theorem shows that the differential-algebraic shadow of the statement is true, but its proof uses the derivation on the function field and has no arithmetic counterpart. A solver should not expect the conjecture itself to fall to a variation of the classical method.

Formalization scope

All statements are over $\mathbb{C}$, with the complex exponential. Tuples are indexed by Fin n, ℚ-linear independence is Mathlib's LinearIndependent ℚ, transcendence degree is Mathlib's Algebra.trdeg, the generated field is IntermediateField.adjoin, and the inequality is between cardinals, so the goal reads (n : Cardinal) ≤ Algebra.trdeg ℚ (adjoin ℚ (Set.range z ∪ Set.range (Complex.exp ∘ z))). Algebraicity is IsAlgebraic ℚ, transcendence is Transcendental ℚ, and algebraic independence is AlgebraicIndependent ℚ.

There is no trivializing formalization here: the hypothesis LinearIndependent ℚ z is satisfiable for every $n$, so the goal is not vacuous, and the conclusion is an inequality of cardinals rather than a statement about a definition introduced for this mission.

The Ax milestone is stated for formal power series in one variable over $\mathbb{C}$: the exponential relation is expressed as the differential equation $g_i' = f_i' g_i$ with PowerSeries.derivative, and the conclusion bounds Algebra.trdeg ℂ of the ℂ-subalgebra generated by the $f_i$ and the $g_i$. The conditional corollary takes the full statement of Schanuel's conjecture as an explicit hypothesis, so it is provable unconditionally as stated.

Infrastructure that a complete development needs, and that is reusable well beyond this mission: Siegel's lemma and height machinery for algebraic numbers, the standard auxiliary-function construction with derivative bounds, and interface lemmas relating Algebra.trdeg, AlgebraicIndependent and Transcendental. Reductions between the milestones — for example deriving Hermite–Lindemann from Lindemann–Weierstrass, or the six exponentials theorem from a general Baker-type statement — are welcome as sketches.

Selected references

• S. Lang, Introduction to Transcendental Numbers, Addison–Wesley, 1966. (Schanuel's conjecture is stated in Chapter III.)
• A. Baker, Linear forms in the logarithms of algebraic numbers I, Mathematika 13 (1966), 204–216. https://doi.org/10.1112/S0025579300003971
• J. Ax, On Schanuel's conjectures, Annals of Mathematics 93 (1971), 252–268. https://doi.org/10.2307/1970774
• A. Macintyre and A. J. Wilkie, On the decidability of the real exponential field, in Kreiseliana, A K Peters, 1996, 441–467.
• M. Waldschmidt, Diophantine Approximation on Linear Algebraic Groups, Springer, 2000.
• Wikipedia, Schanuel's conjecture. https://en.wikipedia.org/wiki/Schanuel%27s_conjecture