I am trying to construct an example of a geometric problem, stated in terms of Euclidean Geometry, that is not Machine Provable (or in an equivalent definition Automatically Provable)-i.e no computer can solve it.
As far as I can tell, the process by which the machine goes about tackling the problem involves transforming it into polynomial expressions, so transcedental numbers seem the obvious choice. So, let's chose a well-known transcedental number, $2^{\sqrt 2}$ (Gelfond–Schneider constant) and state the problem as such:
Given a line segment $a$, of length $2$, and an isosceles right triangle whose sides are of length $1$, can we construct by ruler and compass a line segment equal to $a$ to the power of $b$, where $b$ is the length of the hypotenuse of the given triangle?
This might seem like a superflous way of coming up with $2^{\sqrt 2}$ but I want to make sure that it makes sense in terms of Euclidean Geometry. That is, someone who, say, has only read The Elements would understand it.
So, does this seem to do the trick? Is the problem valid as a strictly euclidean geometry problem, and if so, is it automatically solvable?
One needs a precise definition of "stated in terms of Euclidean geometry." The axioms given by Euclid are imprecise, and incomplete.
If we make them precise, for example by using the first-order axiomatization by Tarski, we have the result of Tarski that the theory is decidable. This is a consequence of the fact that the first-order theory of real-closed fields is decidable.
If we are much looser and allow the introduction of integers, or rationals (say via commensurability) then undecidability is a consequence of the undecidability of the first-order theory of integers, or the first-order theory of rationals.