Tarski's exponential function problem

The question

Tarski's exponential function problem. Is the first-order theory of the real exponential field ${\mathbb{R}}_{\exp }=(\mathbb{R},+,\cdot ,-,0,1,\le ,\exp )$ decidable?

Tarski proved that the first-order theory of the real ordered field $(\mathbb{R},+,\cdot ,-,0,1,\le )$ is decidable, and asked whether the same holds for the real exponential field ${\mathbb{R}}_{\exp }=(\mathbb{R},+,\cdot ,-,0,1,\le ,\exp )$. The problem is open. Macintyre and Wilkie proved that the theory of ${\mathbb{R}}_{\exp }$ is decidable if the real version of Schanuel's conjecture holds.

Decidability of a theory is formalised in FirstOrder.Language.Theory.IsDecidable: the set of consequences of the theory is computable, with respect to the Gödel numbering of sentences from FormalConjecturesForMathlib.ModelTheory.Encoding. The theory in question is the complete theory of ${\mathbb{R}}_{\exp }$, which contains every sentence true in ${\mathbb{R}}_{\exp }$, so this is the same as asking for an algorithm deciding membership (FirstOrder.Language.Theory.isDecidable_completeTheory_iff). The statements use the language of ordered rings with the order symbol ≤ in place of <. Some sources state the problem for $(\mathbb{R},+,\cdot ,\exp )$ instead. Since $<$, $\le$, $-$, $0$ and $1$ are definable from $+$ and $\cdot$, all these structures are interdefinable, and the choice does not affect decidability.

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.Wikipedia.TarskiExponentialFunctionProblem. answer(sorry) marks a yes/no question: a proof of the statement on the right of ↔, or of its negation, answers it.

theorem tarski_exponential_function_problem :
    answer(sorry) ↔ (Language.orderedExpField.completeTheory ℝ).IsDecidable

What counts as progress

• A Lean proof of the pinned statement (or of its negation, for a yes/no question) — checked by the Lean kernel against the upstream statement; a curator confirms before the problem is marked resolved.
• Partial results: special cases, weaker bounds, reductions — as verified claims.
• Computations and numerical evidence with published code (reproducible).
• Literature: the problem may have been solved or partly solved already. Report it as a literature claim.
• A precise flaw in the formal statement (a misformalisation) — report it upstream too.

References

• Wikipedia, Tarski's exponential function problem, listed in Wikipedia, List of unsolved problems in mathematics.
• A. Tarski, A decision method for elementary algebra and geometry, 2nd ed., University of California Press, Berkeley and Los Angeles, 1951.
• A. Macintyre, A. J. Wilkie, On the decidability of the real exponential field, in: P. Odifreddi (ed.), Kreiseliana: about and around Georg Kreisel, A K Peters, Wellesley, MA, 1996, pp. 441–467.
• S. Kuhlmann, Model theory of the real exponential function, Encyclopedia of Mathematics.
• A. Berarducci, F. Gallinaro, On the elementary theory of the real exponential field, arXiv:2603.08365 (2026). Assuming Schanuel's conjecture, gives an axiomatisation of the theory of ${\mathbb{R}}_{\exp }$ and recovers the Macintyre–Wilkie decidability result.

Source and licence

Imported from Formal Conjectures (Wikipedia), commit e6d1743831c2. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.