Euclidean geometry theorem proving complexity
It is common to prove the decidability of first-order Euclidean geometry by encoding the language of Euclidean geometry into the language of real closed fields and then showing that the latter is decidable. A singly-exponential space upper bound on deciding the first-order theory of real closed fields was proven in Ben-Or, Kozen, and Reif (1986). This implies a doubly-exponential time upper bound.
I believe this is the best known complexity for the decision problem for general first-order sentences in the language of real closed fields. However, I am not sure whether deciding real closed fields is equivalent (bidirectionally) to deciding Euclidean geometry, since a typical encoding of (say) the language of Tarski's axioms into the language of real closed fields only uses a small subset of the possible polynomials. So maybe first-order Euclidean geometry can be decided with lower complexity than this. It is at least PSPACE-hard, since TQBF is easily encoded into first-order Euclidean geometry.