A language is said to have *quantifier elimination* if every first-order-logic sentence in the language can be shown to be equivalent to a quantifier-free sentence, i.e., a sentence without any $\forall$s or $\exists$s. An example is the theory of real closed fields (such as $\mathbb{R}$), considered with the four basic operations, equality ($=$) and inequalities ($<$, $>$).

Question: how fast could an algorithm that does quantifier elimination be? By how much are current algorithms (such as the ones that proceed by cylindrical decomposition) worse than the best algorithms that are conceivably possible? What are, in brief, the main open computational problems in quantifier elimination?

(We can try to restrict the discussion to $\mathbb{R}$, though other "useful" theories also interest me.)

As far as I know, the situation is as follows: in general, there are first-order sentences on $k$ variables that are not equivalent to any quantifier-free sentences of length less than $\exp(\exp(C k))$; this means, in particular, that the worst-case performance of a quantifier elimination program has to be at least doubly exponential on $k$. This is matched by cylindrical-decomposition algorithms (correct me if I am wrong). At the same time, if the original formula contains only $\exists$s or only $\forall$s, then an algorithm that is singly exponential on $k$ is known. (I'm going by a very quick reading of Basu, Pollack, Roy, Algorithms in Real Algebraic Geometry; all errors are my own.)

The second case - on which exponential bounds are known - is important, since it covers all cases of the form "prove this formula holds for all $x_1, x_2,\cdots, x_k$".

Is this the end of the story, or is there a subarea where plenty of work could remain to be done?

Well, there seems to be real interest in this question, but no answer as such yet. Let me suggest what would be very nice as an answer: a few open problems on the subject, hard but not impracticable, with statements that are neat enough for mathematicians yet also close enough to actual practice that their solution would likely be useful.

For example: would reducing the existential theory of $\mathbb{R}$ to $k$-SAT be such a problem?