Is it theotically possible to create a machine that could randomly generate any elementary geometric problems/theorem? Refering back to this quesion: Is it true that all of the euclidean geometry problem in the IMO(international mathematical olympiad) could all be solve by the analytical geometry? , we know that any elemetary geometry problem could be solved by computer in finite amount of time.
So, conversely, is it theotically possible to create a machine that could randomly generate any elementary geometric problems/theorem?
 A: Suppose we formalize elementary geometry, say the plane version, using say Tarski's formalization (there are others).  Then of course we can generate all well-formed sentences.  As to the "randomly" part, we could use a pseudo-random number generator. If that is not good enough, I have no algorithmic suggestion. 
Note that the axioms of Tarski's geometry are a recursive set. Therefore, as noted in the answer by apt1002, we can not only algorithmically list all sentences, we can algorithmically list all proofs. (A proof is just a special kind of finite list of sentences.)
Tarski's theory is complete. Therefore, in principle, to verify whether a sentence $\phi$ is a theorem, we just list all proofs. If $\phi$ appears at the end of a proof, then $\varphi$ is a theorem. If $\lnot\varphi$ appears at the end of a proof, then $\varphi$ is not a theorem. This procedure must terminare, so we have an algorithm.
Of course it is a terrible algorithm. Tarski's algorithm for the theory of real-closed fields, and the various implementations since, are far more efficient.  
A: Yes. Proofs are ennumerable by a computer.
