Tarskis Exponential Function Problem

### What is the conjecture

Let $\mathbb{R}$ denote the real numbers with addition $(+)$, multiplication $(\cdot)$, and the exponential function $\exp$. The problem asks whether the first-order theory of the structure $(\mathbb{R}, +, \cdot, \exp)$ is decidable. That is, does there exist an effective algorithm (a Turing machine) that, given any first-order sentence $\phi$ in the language $\{+, \cdot, \exp\}$, can determine in finite time whether $\phi$ is true in the standard model $(\mathbb{R}, +, \cdot, \exp)$ or not?

Alfred Tarski proved that the theory of $(\mathbb{R}, +, \cdot)$ without the exponential function is decidable. However, adding the exponential function significantly complicates the problem. The decidability of $\text{Th}(\mathbb{R}, +, \cdot, \exp)$ remains open. The problem can be equivalently stated as: does there exist an effective procedure for determining whether any given exponential polynomial in $n$ variables with integer coefficients has a solution in $\mathbb{R}^n$?

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

**Sources:**
- https://en.wikipedia.org/wiki/Tarski's_exponential_function_problem, http://garden.irmacs.sfu.ca/op/tarskis_exponential_function_problem, https://www.sciencedirect.com/science/article/pii/S0049237X08718111, https://encyclopediaofmath.org/wiki/Model_theory_of_the_real_exponential_function

### Prerequisites needed

**Formalizability Rating:** 4/5 (0 is best) (as of 2026-01-21)

Formalizing Tarski's exponential function problem requires significant foundational work in mathematical logic and model theory. Mathlib has basic real number theory and algebraic structures, but lacks formalized model-theoretic concepts needed for this problem. Specifically needed: (1) A formal definition of first-order sentences and their satisfaction in a model; (2) Decidability and computability theory definitions in the Lean/Mathlib context; (3) The formal structure of the real exponential field with its language; (4) Exponential polynomials and their properties. While the problem statement itself can likely be written, the proof or disproof would require developing substantial theory around decidability of real closed fields with transcendental functions.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-03

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

---
This issue was generated by an AI agent.

See more here: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)

Feedback on mistakes/hallucinations: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Issue.20Agent.20Feedback.20Topic/with/569223911)

No target file, test, or Lean entry point is specified. Start by reviewing existing formalized conjectures in the formal-conjectures repository and the cited sources, then determine how this statement fits the repository's conventions. Done means adding a correct formal statement of Tarski's exponential function problem, not resolving the open problem.

Written by the indexing model from the issue text.