IMO Grand Challenge • Hacker News Board

Re: IMO Grand Challenge

#61

Post by OscarCunningham » Sat, Oct 26, 2019, 8:42 PM UTC

woopwoop wrote: post #60

OscarCunningham wrote: post #40

Earlier quoted context omitted.

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. Af…

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/…

That question was asked by Kevin Buzzard, who is on the IMO Grand Challenge committee. So we are really going over old ground here.

Re: IMO Grand Challenge

#62

Post by woopwoop » Sat, Oct 26, 2019, 9:14 PM UTC

OscarCunningham wrote: post #61

woopwoop wrote: post #60

Earlier quoted context omitted.

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/…

That question was asked by Kevin Buzzard, who is on the IMO Grand Challenge committee. So we are really going over old ground here.

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.

Re: IMO Grand Challenge

#63

Post by buyingarmor » Sat, Oct 26, 2019, 9:28 PM UTC

>10 minutes (which is approximately the amount of time it takes a human judge to judge a human’s solution)

Hah, some student solutions take hours to read...

Re: IMO Grand Challenge

#64

Post by MauranKilom » Sat, Oct 26, 2019, 10:00 PM UTC

elil17 wrote: post #42

lordnacho wrote: post #26

Earlier quoted context omitted.

Perhaps brute force is the wrong term, but at least they would require a chain of transformations that a human could easily mess up. Rearranging, substituting, etc. A machine wouldn't get that wrong ever, whereas a human would have wasted a fair bit of time. Well I did miss the IMO team narrowly, but I didn't think those questions were all that different in nature. Quirky questions you'd never see in school, but solv…

You should take a look at the IMO problems - they are generally very different from any sort of math problem you’ve ever seen before. For instance: Determine all finite sets S of at least three points in the plane which satisfy the following condition: for any two distinct points A and B in S, the perpendicular bisector of the line segment AB is an axis of symmetry for S. This is a deeply abstract and complex problem…

That was an IMO problem? How long ago was this? I'm just surprised because I found the solution set + proof in like 5 minutes of writing elementary observations on a sheet of paper... (Very much unlike the IMO qualifying test I took a few years ago. Couldn't even produce a meaningful sketch of the geometry in question there...)

--- quick solution sketch ---

- every regular polygon is an obvious solution

- no three points can be collinear (can't have distinct parallel symmetry axes)

- for a given solution, look at all (3+) symmetry axes - they have to meet at the same point (easy to prove by contradiction)

- thus the angles between "neighboring" axes must be constant, namely PI / n for a solution with n distinct axes

- since any solution has to fulfill the above, for a given n > 2 we can draw all the axes (intersection point and "phase" are degrees of freedom). Add one point and mirror it on all axes - if no new axes are added (and you now have > 2 points, i.e. didn't put the initial point at the center) it's a valid solution. (You can't add another point afterwards - it would form a new axis with the first one).

- some footwork left to conclude that only "starting points" that produce regular polygons fulfill that. A proof by contradiction is pretty obvious in a sketch, but takes some effort to get even/odd n-gons covered correctly - there's probably something more elegant, but at this point you already know you've got the proof down.

While writing this out I realized that all the points must lie on a circle (apply circle chord perpendicular bisector theorem to "successive" point pairs) which should help simplify the proof.

(Please point out any mistake/misunderstanding - the solution seems way too trivial for an IMO problem. Well, a recent one at least.)

Re: IMO Grand Challenge

#65

Post by OscarCunningham » Sat, Oct 26, 2019, 10:04 PM UTC

woopwoop wrote: post #62

OscarCunningham wrote: post #61

Earlier quoted context omitted.

That question was asked by Kevin Buzzard, who is on the IMO Grand Challenge committee. So we are really going over old ground here.

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).

Re: IMO Grand Challenge

#66

Post by andrepd » Sat, Oct 26, 2019, 10:06 PM UTC

pirocks wrote: post #56

I'm curious as to whether LEAN is the right choice for this. LEAN is rather hard to parse, and complex, as a consequence of being designed for use by humans. Perhaps specifying the problem(s) in a small superset of first order logic would be better?

The people promoting this are the Lean developers... :p

Re: IMO Grand Challenge

#67

Post by robocat » Sat, Oct 26, 2019, 10:31 PM UTC

> but there are no other limits on the computational resources it may use during that time

I am guessing that defining a CO₂ or $ limit causes problems.

They could specify that the solution must be CO₂ neutral e.g. suggest an official CO₂ offset provider?

Re: IMO Grand Challenge

#68

Post by monktastic1 » Sat, Oct 26, 2019, 10:56 PM UTC

mkagenius wrote: post #59

Not sure if reading the problem text and understanding what it is asking is part of the problem or not. If it is, well, good luck collecting data for it.

This is explained in paragraph two of the post. No, that is not part of the problem.

Re: IMO Grand Challenge

#69

Post by deepnotderp » Sat, Oct 26, 2019, 11:07 PM UTC

throwaway-ai-ai wrote: post #10

I'm curious: what are people's predictions for when it will be possible to run some program XYZ on a $10/hr EC2 machine and have it beat humans on the IOI/ICPC ? Furthermore, suppose such an open source program existed, how long would it take for it to start replacing remote contractors and then in-office programmers? ["start replacing" as in, say, 10% of human programmers]

Program synthesis of large programs is an incredibly difficult problem. I could definitely be wrong but I don't think it's solvable with current AI techniques.

Re: IMO Grand Challenge

#70

Post by saagarjha » Sat, Oct 26, 2019, 11:13 PM UTC

MauranKilom wrote: post #64

elil17 wrote: post #42

Earlier quoted context omitted.

You should take a look at the IMO problems - they are generally very different from any sort of math problem you’ve ever seen before. For instance: Determine all finite sets S of at least three points in the plane which satisfy the following condition: for any two distinct points A and B in S, the perpendicular bisector of the line segment AB is an axis of symmetry for S. This is a deeply abstract and complex problem…

That was an IMO problem? How long ago was this? I'm just surprised because I found the solution set + proof in like 5 minutes of writing elementary observations on a sheet of paper... (Very much unlike the IMO qualifying test I took a few years ago. Couldn't even produce a meaningful sketch of the geometry in question there...) --- quick solution sketch --- - every regular polygon is an obvious solution - no three po…

It’s from 1999. I’d agree that this is a relatively easy problem; I think I’ve seen harder questions on the AMC…