A lot of IMO geometry problems are easy for computers because they can simply use coordinates to convert the problem to algebra (this approach is computation heavy which is why humans don't use it even though it's guaranteed to work given enough time). So in a good year the computer might get two out of the six problems without having to do anything clever.
I think this illustrates one of the preconceptions this challenge is meant to work against. Namely, people think of coordinate bashing as "computational" and purely synthetic/geometric solutions as "insightful". But there's no reason that a computer would find the second way more difficult. After all, synthetic geometry is just another system of rules, like ordinary algebra.
Us humans might fall back on coordinate bashing, but that's just because we have a lot of practice with the rules of algebra. To a computer, one rule set is as good as any other. What we call geometric insight boils down to pattern matching configurations to previously seen ones, combined with search in the space of possible moves, both of which computers can do.
The current situation doesn't reflect that though. We have a algorithm (Gröbner bases) for doing coordinate bashes which is guaranteed to succeed, whereas as far as I know we don't have an analogous algorithm in terms of synthetic geometry (other than the direct translation of coordinate bashing).
Sure, but I don't think theoretical guarantees are that important in practice. When I solve math problems, I don't personally use methods with such guarantees. Mathematica has certain guarantees for evaluating integrals, but that really doesn't help when it chokes for an hour on one. In practice what matters is computational complexity, and how well heuristics can help you narrow down your search space. And here IMO geometry problems have the enormous advantage that one knows there exists a short, purely synthetic solution.
The kind of problems I'm thinking of are those like 2 and 6 on this year's IMO.
You have a bunch of points, lines and circles in some configuration and you have to prove that some condition holds. So you assign symbols to represent the coordinates of each of these points and you represent each fact you are told about them by some equation. The condition you are trying to prove is also represented by some equation. After multiplying up to get rid of square roots each of these equations is setting a polynomial equal to 0. So you are just trying to prove that some polynomial must be 0 if a bunch of other polynomials are 0, which can be done algorithmically via Gröbner bases.
There is a Mathoverflow thread [0] about this. Discussion in the comments expresses skepticism because olympiad questions usually involve questions about choosing specific real roots of polynomials, not just arbitrary roots. The discussion there mostly suggests using some principles in real algebraic geometry, but these seem to be too slow and complicated to use in practice at this time.
I'm a little perplexed by the dismissiveness of your response (perhaps I'm misreading?). I'm not saying IMO problems will never be algorithmically approachable, just saying expressing these problems in terms of Grobner bases may be harder than is suggested here. Buzzard also expresses skepticism about using Grobner bases for these sorts of problems in the comments.
I wasn't trying to be dismissive, just saying that I didn't have much to add that wasn't already said there (and separately pointing out the connection between Buzzard and this thread).
What do you mean "by coordinates"? If you are asked to show that three points are on a line, having an accurate diagram is not enough, is it? Isn't the task to use the constraints presented (these lines are parallel, this is a right angle, etc) in a step-based reasoning for whatever you're asked to prove?
It is done using symbolic algebra, not just assigning specific coordinates if that's what you're asking.
Let's say you're given three parallel lines. You can put your x axis along the first line. Then its equation is y = 0. The other two lines necessarily have equations y = a and y = b for some reals a and b. Then you calculate the other quantities involved via a and b and other parameters you have to introduce. At the end you calculate the coordinates of your three points and verify, symbolically, that they lie on the same line.
Yes, that's right. You end up with a system of equations and solve it. So what does "by coordinates" mean? Is the original commenter simply saying that the machine will always be able to solve that system? He's right if that is what he means. Originally it sounded like "the machine can read the diagram accurately".
