The problems from IMO 2009 are now available. I haven’t had much time to work on them, though.
There are two classical geometry problems, which I already know I won’t attempt. While I am well aware that classical geometry often requires a great deal of ingenuity, I am also aware of the existence of the field of automatic geometric theorem proving. On this subject I largely agree with Doron Zeilberger: it is more interesting to find an algorithm to prove classes of theorems than to prove individual theorems. The sooner we see areas like classical geometry as “low-level,” the sooner we can work on the really interesting “high-level” stuff. (Plus, I’m not very good at classical geometry.)
Zeilberger’s typical example of a type of theorem with a proof system is the addition or multiplication of very large numbers: it is more interesting to prove 
But so I can make my point concretely, I’d like to discuss some examples based on the types of problems most of us had to deal with in middle or high school.
be the ordinary generating function for the ordered rooted trees on 
vertices (essentially we ignore the root as a vertex). This is one of the familiar definitions of the 
.
describes the species 
of sequences. So what this definition means is that, after tossing out the root, an ordered rooted tree is equivalent to a sequence of ordered rooted trees (counting their roots) in the obvious way; the roots of these trees are precisely the neighbors of the original root. Multiplying out gets us a quadratic equation we can use to find the usual closed form of 
, but we can instead recursively apply the above to obtain the beautiful continued fraction
.
