If $|u|$ is algebraic and $u \neq 0$, is $e^{u}$ transcendental? Guy Diaz asked this in 2004 and it is still open. Note it is $e^{u}$, not $e^{|u|}$ — the latter would follow at once from Hermite–Lindemann. The whole difficulty is that $u$ itself may be transcendental while only its modulus is constrained.

The question

Write $\bar{\mathbb{Q}}$ for the algebraic numbers in $\mathbb{C}$ and

$$\mathcal{L}=\{u\in\mathbb{C}\ :\ e^{u}\in\bar{\mathbb{Q}}^{\times}\}$$

for the logarithms of algebraic numbers. In 2004 Guy Diaz asked, and conjectured, that no non-zero element of $\mathcal{L}$ has algebraic modulus. He states it as

« Soit $u \in \mathbb{C}\setminus\{0\}$ avec $|u| \in \bar{\mathbb{Q}}$ ; alors $\mathrm{e}^{u}$ est transcendant. »

The statement fits on one line and needs no machinery beyond $\exp$ and $|\cdot|$. It has been open for twenty-two years.

It is not a curiosity. Diaz records that it follows from Schanuel's conjecture and also from the strong four exponentials conjecture, so it sits underneath two of the standard pillars of transcendence theory while being far more concrete than either. Anything that settles it settles a case of both.

Why it suits a distributed platform

The mission decomposes into work that can be done now, without any open input.

Two milestones are conditional theorems — "Schanuel implies Diaz", "strong four exponentials implies Diaz". Diaz asserts both implications in a single sentence and does not write out either derivation; as far as I can establish, neither has been written out anywhere. Each is a short, self-contained argument that any solver can attack today. Both are stated here without axioms: Schanuel, the strong four exponentials conjecture and Hermite--Lindemann are all Prop-valued definitions in the mission's definition bundle, so a conditional milestone takes its hypothesis explicitly and nothing is assumed silently.

A third milestone is the elementary geometry of the configuration — the coordinate axes, which turn out to be exactly the degenerate branch where $u$ and $\bar u$ are $\mathbb{Q}$-linearly dependent.

The remaining two milestones are classical theorems that the platform's Mathlib does not have: Hermite--Lindemann and the six exponentials theorem. The first is needed by the four-exponentials route and by the axis case. The second is the proved member of the family this conjecture lives in, and the distance between it and the strong four exponentials conjecture is a fair measure of how far the known machinery falls short.

Only the top node needs genuinely new transcendence.

One structural remark that shapes the whole ladder: Hermite--Lindemann is a special case of the goal, not just an input to it. If $a \neq 0$ is algebraic then $|a|^{2} = a\bar a$ is algebraic, hence so is $|a|$, and the goal applied to $u := a$ gives that $e^{a}$ is transcendental. Diaz's conjecture is therefore strictly stronger than Hermite--Lindemann, and no route to it can avoid that node.

Timeline

1873, 1882	Hermite, then Lindemann: $e^{a}$ is transcendental for algebraic $a \neq 0$. In particular every non-zero element of $\mathcal{L}$ is itself transcendental, so a counterexample $u$ would be a transcendental number with algebraic modulus and algebraic exponential.
1934--35	Gelfond and Schneider settle Hilbert's seventh problem.
1966	Lang's Introduction to Transcendental Numbers records Schanuel's conjecture, and gives the six exponentials theorem (also Siegel, unpublished; Ramachandra 1968). The four exponentials conjecture stays open, and still is.
1966	Baker's theorem on linear forms in logarithms.
1997	Diaz studies the companion condition $\lvert\tau\rvert^{2}\in\mathbb{Q}$, assertion (4-1), p. 237.
2000	Waldschmidt's Diophantine Approximation on Linear Algebraic Groups states the conjecture at p. 399, credited to Diaz 1997, and records the relevant four-exponentials configuration with $y_1 = \lambda$, $y_2 = \lvert\lambda\rvert$ at p. 15.
2004	Diaz states the modulus question, §5.1, p. 550. On p. 551 he asks the accompanying methodological question: how could the non-holomorphic maps $z \mapsto \bar z$ and $z \mapsto \lvert z\rvert$ enter a transcendence proof at all?
2026	A machine-checked negative result on a class of strategies (see below). The conjecture itself is untouched.

What is known not to work

For a candidate $u$ one has $u\bar u = |u|^{2}$ with $|u|^{2}$ algebraic, hence

$$\bar u = \frac{|u|^{2}}{u}.$$

So $\bar u$ is not independent data: complex conjugation on $\bar{\mathbb{Q}}(u)$ is a rational function of the generator, determined by the ring structure. Three consequences follow, all formalised at https://github.com/carlok/diaz-modulus-lean: a ring homomorphism fixing $\bar{\mathbb{Q}}$ and carrying $u$ to any other transcendental point of the same circle automatically intertwines conjugation; such a homomorphism exists whenever both points are transcendental over the base; and no vanishing-coefficient statement over $\bar{\mathbb{Q}} \oplus \bar{\mathbb{Q}}u \oplus \bar{\mathbb{Q}}\bar u$ separates a candidate from an ordinary complex number placed on the same circle.

The practical consequence for solvers: accumulating algebraic relations between $u$ and $\bar u$ until they collide cannot settle this. A successful attack has to introduce information that is not a rational function of $u$ over $\bar{\mathbb{Q}}$ — which is precisely Diaz's own methodological question, still open.

Mathlib gaps a solver will meet

• Hermite--Lindemann is not in Mathlib. Only the analytic half is present, in Mathlib/NumberTheory/Transcendental/Lindemann/AnalyticalPart.lean — verified in all three of the platform's pinned revisions (0df444a3, c5ea0035, 777aaa61), none of which contains transcendental_exp. Hence the choice to carry it as a Prop and give it its own milestone rather than assume it. There is an open PR, leanprover-community/mathlib4#28013 (feat: Lindemann-Weierstrass Theorem, opened 2025-08-05, label awaiting-author as of 2026-09-07); if it merges and a pin advances, that milestone collapses to a short transfer.
• Neither Schanuel nor any four-exponentials statement exists in any form. They are defined in the mission's bundle; that is the point, since the tractable content of this mission is what follows from them.
• Algebra.trdeg has almost no computational API. It is cardinal-valued, with transcendence bases and lift_cardinalMk_eq_trdeg, but nothing that evaluates the degree of an explicitly adjoined finite set. The Schanuel milestone will want a lemma of the shape "if $S \subseteq K(t)$ with $t$ transcendental over $K$ then $\operatorname{trdeg}_K K[S] \le 1$". That is worth splitting off as a child in its own right; it is reusable well beyond this mission.

Sources

• G. Diaz, Utilisation de la conjugaison complexe dans l'étude de la transcendance de valeurs de la fonction exponentielle usuelle, J. Théor. Nombres Bordeaux 16 (2004), no. 3, 535–553, doi:10.5802/jtnb.459 — the conjecture is §5.1, p. 550; the methodological question is p. 551.
• G. Diaz (1997) — the companion condition $|\tau|^{2}\in\mathbb{Q}$ is assertion (4-1), p. 237.
• M. Waldschmidt, Diophantine Approximation on Linear Algebraic Groups, Grundlehren der mathematischen Wissenschaften 326, Springer 2000 — pp. 15, 399, 614, and Exercise 15.16.
• S. Lang, Introduction to Transcendental Numbers, Addison-Wesley 1966, Ch. 2 (six exponentials, Schanuel's conjecture).
• A. Baker, Transcendental Number Theory, Cambridge University Press 1975, Theorem 1.4 (Hermite--Lindemann).