Is $ \pi $ definable in $(\Bbb R,0,1,+,×, <,\exp) $?
Is there a first-order formula $\phi(x) $ with exactly one free variable $ x $ in the language of ordered fields together with the unary function symbol $ \exp $ such that in the standard interpretation of this language in $\Bbb R $ (where $ \exp $ is interpreted as the exponential function $ x \mapsto e^x $), $\phi (x) $ holds iff $ x=\pi $?
EDIT: As Levon pointed out, a negative answer to this problem would imply that $π$ and $e$ (and $e^e$, $(2e)^{3e^2}$, and so on) are algebraically independent over $\Bbb Q$, which is an unsolved problem. So, if you think that a definition of $\pi$ is impossible, I would be pleased if you could show something like, that it is possible to reduce $\phi$ to a formula which contains no terms involving bound variables inside exponential functions, which would reduce the problem more or less to a question on algebraical independece. However because there are such intricate connections between exponential and trigonometric functions, I don't think that $\pi$ should be undefinable.
Solution 1:
Todd Trimble provided the answer to this question on MO:
Assuming Shanuel's conjecture, this treatise about exponential rings proves that (see Theorem 2.5.1) the exponential ring generated by $\pi$ looks just as the exponential ring generated by nearly every other real number, which implies that there is no defining relation of $\pi$ over $\Bbb R_{\exp}$.