It is a well-known result that the first-order theory of the real numbers is decidable. However the decision algorithm for this language is in double exponential time, so such an algorithm cannot be practically applied. It then seems perfectly consistent that there is some open problem expressible in the first-order theory of the reals, which the decision algorithm could solve if given enough time.
Does anyone know of any such problem?
If not, as a softer question, does anyone know of a simple statement in the first-order theory of the real numbers that is difficult to prove?
By some wonderful coincidence this was just covered unprompted in a lecture I attended, where it was mentioned the kissing number problem in, say, 5 dimensions is an open problem equivalent to a first order sentence in the language of the reals and hence decidable by an algorithm given enough time.