According to Marker's ["Model Theory: An Introduction"][1], the real exponential field has a $\forall\exists$ axiomatization (because it is model complete) but no-one has any idea what such an axiomatization might look like. Has any progress been made on this since  the early 2000s when Marker wrote this?


  [1]: http://link.springer.com/book/10.1007/b98860/page/1