4 ms·

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 hav

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.

pfortuny 7y ago
Yes: those problems will boil down to: do some functions (polynomials) belong to an ideal (maximal, usually)? Grobner it and you are done.
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 ago
  That 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 ago
    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.
    - OscarCunningham 7y ago
      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).

pfortuny 7y ago

Yes: those problems will boil down to: do some functions (polynomials) belong to an ideal (maximal, usually)? Grobner it and you are done.

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 ago
That 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 ago
  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.
  - OscarCunningham 7y ago
    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).