On the automated solution of Olympiad problems This is a soft question on developing software to solve  exam/contest problems.
Imagine the following scenario: You, as user, have  (say) an IMO exam paper. You type one question at a time, perhaps in some machine-readable format, into a command-line interface like Matlab.  A minute of thinking later, your program spits out the answer (and also the needed proof/derivation steps), and perhaps in 15 minutes, you have solved the entire paper with electronic assistance, but for which your score would have been 42/42. You also have the confidence that your answer has been checked and cross checked by your Silicon-powered friend. Further, suppose you were to show the output to an IMO judge, (s)he would have no hesitation in awarding a full score, except for the fact that it takes a little effort to read the "machine-like" format of the output.
A crude design would have Matlab (for computation) and Mizar (for logical reasoning) at the back-end, and if needed a natural language processing engine at the front end. Note that there are 2 big hurdles as I see it:


*

* The natural language engine would have to be very sophisticated to understand the subtleties of maths problems, expressed in English.

* Existing software like Matlab is probably better suited for problems fitting a template (say matrix inversion), but not much use for say, a functional equation to be solved by a clever trick. An examiner can always come up with a new "clever trick" beyond what the software designers have thought of.


Question: Is there one such tool in existence? Would anyone be interested if it's developed ? Any open-ended comments?
As an aside,this tool if  developed may be applied to a wide variety of exams ( GRE, SAT, "Engineering entrance" exams in India) ; we may have a student and a computer taking the exam side by side to determine the strengths and weaknesses of such software.
 A: Most IMO problems are not immediately translatable (by a human) into sentences in a decidable theory.  Some geometry and algebra problems and probably a few types of number theory problems have mechanical solution algorithms, such as quantifier elimination.  A subset of those problems are presented in machine-interpretable form such as a system of equations with the word "solve".  
Beyond that limited subset of problems, you are asking whether unassisted natural language processing and AI could be built or would be useful.
A: I doubt one could ever write such a program to solve all IMO problems. What really makes IMO problems so much "easier" than research maths that we can't do? Many IMO problems allude to very difficult mathematics recently or currently in research. However, for certain types of IMO problems, automated algorithims already exist which solve them in a routine fashion. For example, Algebraic Geometry has reduced Euclidean geometry problems into rountinely verifying certain algebraic statements. I can't remember a programs name that does this, but it certainly exists. 
There is no Turing machine which will output a proof of any input theorem (or even output whether the theorem is true or false), and there is no bound to the length of the proof of a theorem dependent on the length of the theorem, so even simple statements can have extremely long proofs incomprehensible to humans. So to expect we will ever write such a program is probably naïve. 

See this and the references therein for information on automated theorem proving in geometry.
