3 ms·
There is a Mathoverflow thread [0] about this. Discussion in the comments expresses skepticism because olympiad questions usually involve questions about choosi
by woopwoop 7y ago
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.
[0] https://mathoverflow.net/questions/337558/automatically-solving-olympiad-geometry-problems https://mathoverflow.net/questions/337558/automatically-solv...
- OscarCunningham 7y agoThat question was asked by Kevin Buzzard, who is on the IMO Grand Challenge committee. So we are really going over old ground here.
- woopwoop 7y agoI'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.
- OscarCunningham 7y agoI 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).