TarskiExponentialFunctionProblem.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

5 declarations, 3 contain sorry, 0 declared as axioms

Tarski's exponential function problem

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.

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.

Imports (1)

FormalConjecturesUtil

theorem TarskiExponentialFunctionProblem.isDecidable_completeTheory_real_orderedField Tarski's theorem sorry line 66 source
Source documentation
Tarski's theorem. The first-order theory of the real ordered field $(\mathbb{R}, +, \cdot, -, 0, 1, \le)$ is decidable.

depends on sorry what this means
Statement uses: FirstOrder.Language.Theory.IsDecidable, FirstOrder.Language.sum, FirstOrder.Language.ring, FirstOrder.Language.order, FirstOrder.Language.completeTheory, Real
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
35 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem isDecidable_completeTheory_real_orderedField :
    ((Language.ring.sum Language.order).completeTheory ℝ).IsDecidable := by
…
```
theorem TarskiExponentialFunctionProblem.tarski_exponential_function_problem Tarski's exponential function problem sorry line 75 source
Source documentation
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?

depends on sorry what this means
Statement uses: Iff, True, FirstOrder.Language.Theory.IsDecidable, FirstOrder.Language.orderedExpField, FirstOrder.Language.ring, FirstOrder.Language.sum, FirstOrder.Language.exp, FirstOrder.Language.order, FirstOrder.Language.completeTheory, Real
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
41 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem tarski_exponential_function_problem :
    answer(sorry) ↔ (Language.orderedExpField.completeTheory ℝ).IsDecidable := by
…
```
def TarskiExponentialFunctionProblem.RealSchanuelConjecture Documented declaration: RealSchanuelConjecture line 86 source
Source documentation
The real version of Schanuel's conjecture: if $x_1, \ldots, x_n$ are real numbers that are linearly independent over $\mathbb{Q}$, then the field $\mathbb{Q}(x_1, \ldots, x_n, e^{x_1}, \ldots, e^{x_n})$ has transcendence degree at least $n$ over $\mathbb{Q}$.
It is the special case of real arguments of Schanuel's conjecture, which is stated for complex numbers as Schanuel.schanuel_conjecture.

standard axioms: Classical.choice, Quot.sound, propext what this means
Proof uses: Nat, Fin, Real, LinearIndependent, Rat, LE.le, Cardinal, Algebra.trdeg, Subtype, Membership.mem, IntermediateField, IntermediateField.adjoin, Union.union, Set, Set.range, Function.comp, Real.exp
33 instances, coercions and auxiliary constants left out.
```
def RealSchanuelConjecture : Prop :=
…
```
theorem TarskiExponentialFunctionProblem.realSchanuelConjecture_of_schanuelConjecture Schanuel's conjecture for complex numbers, as stated in Schanuel.schanuel_conjecture, implies its real version line 93 source
Source documentation
Schanuel's conjecture for complex numbers, as stated in Schanuel.schanuel_conjecture, implies its real version.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Complex, LinearIndependent, Rat, LE.le, Cardinal, Algebra.trdeg, Subtype, Membership.mem, IntermediateField, IntermediateField.adjoin, Union.union, Set, Set.range, Function.comp, Complex.exp, TarskiExponentialFunctionProblem.RealSchanuelConjecture
Proof uses: Real, AlgHom, AlgHom.restrictScalars, Complex.ofRealAm, LinearIndependent.map', AlgHom.toLinearMap, Iff.mpr, Eq, Submodule, LinearMap.ker, RingHom.id, Bot.bot, Function.Injective, LinearMap, LinearMap.ker_eq_bot, Complex.ofReal_injective, Real.exp, funext, Eq.symm, Complex.ofReal_exp and 10 more
121 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
theorem realSchanuelConjecture_of_schanuelConjecture
    (h : ∀ (n : ℕ) (z : Fin n → ℂ), LinearIndependent ℚ z →
      n ≤ Algebra.trdeg ℚ
        (IntermediateField.adjoin ℚ (Set.range z ∪ Set.range (Complex.exp ∘ z)))) :
    RealSchanuelConjecture := by
…
```
Mentions: TarskiExponentialFunctionProblem.RealSchanuelConjecture
theorem TarskiExponentialFunctionProblem.isDecidable_completeTheory_realExp_of_realSchanuelConjecture Macintyre–Wilkie sorry line 112 source
Source documentation
Macintyre–Wilkie. If the real version of Schanuel's conjecture holds, then the first-order theory of the real exponential field is decidable.

depends on sorry what this means
Statement uses: TarskiExponentialFunctionProblem.RealSchanuelConjecture, FirstOrder.Language.Theory.IsDecidable, FirstOrder.Language.orderedExpField, FirstOrder.Language.ring, FirstOrder.Language.sum, FirstOrder.Language.exp, FirstOrder.Language.order, FirstOrder.Language.completeTheory, Real
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
41 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem isDecidable_completeTheory_realExp_of_realSchanuelConjecture
    (h : RealSchanuelConjecture) :
    (Language.orderedExpField.completeTheory ℝ).IsDecidable := by
…
```
Mentions: TarskiExponentialFunctionProblem.RealSchanuelConjecture