Is every o-minimal expansion of the real field exponentially bounded?

An expansion of the real ordered field $\bar{\mathbb{R}} = (\mathbb{R}, \le, +, \cdot)$ is
*exponentially bounded* if every definable function $f : \mathbb{R} \to \mathbb{R}$ satisfies
$f(t) = O(\exp_N(t))$ as $t \to +\infty$ for some compositional iterate $\exp_N$ of $\exp$.
All known o-minimal expansions of $\bar{\mathbb{R}}$ are exponentially bounded. Van den Dries
and Miller (Duke Math. J. 84 (1996), 497–540, remark following 5.5) write that they do not know
whether there is an o-minimal expansion of $\bar{\mathbb{R}}$ that is not.

Wikipedia's list of unsolved problems states the equivalent question "Does there exist an
o-minimal first order theory with a trans-exponential (rapid growth) function?", where $f$ is
*trans-exponential* if it eventually exceeds every iterate of $\exp$. The two forms agree for
expansions of $\bar{\mathbb{R}}$ by Miller's growth dichotomy (Proc. Amer. Math. Soc. 122
(1994), 257–259): a non-polynomially-bounded o-minimal expansion of $\bar{\mathbb{R}}$ defines
$\exp$.

Formalising this needs o-minimality, which Mathlib does not have, so it goes in
`FormalConjecturesForMathlib/`. It also uses the structures on `ℝ` added by #5385.

AMS: 3 (model theory), 26 (real functions).

The issue points to FormalConjecturesForMathlib/ and the structures on ℝ added by #5385. First determine how to state o-minimality and exponential boundedness in Lean; no specific file or test is named. Done means the stated equivalent question has a precise Lean formalization.

Written by the indexing model from the issue text.