IMO Grand Challenge
imo-grand-challenge.github.io
imo-grand-challenge.github.io
these three points are on one line
these three lines intersect at one point
these two lines are parallel
these four points are on a circle
these two angles are equal
etc ...
There are things that absolutely can be done via coordinates, if one can brute force large algebraic expressions.
If memory serves right, there's a certain subset of geometry that decidable in that way. Ie you can just run an algorithm.
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.
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.
Grobner it and you are done.
[0] https://mathoverflow.net/questions/337558/automatically-solv...
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 AI must be open-source, released publicly before the first day of the IMO, and be easily reproduceable. (sic) The AI cannot query the Internet.
Based on what? An AI which could reliably produce proofs for these problems would be at the cutting edge of research. Putting additional constraints on it for "fairness" just increases the likelihood of failure. It's not as if there's already some competition to measure up against.
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]
A chess program can be trained on a EC2 instance that can possibly beat most grandmasters. My best guess, people will get over it and move on to more difficult challenges. The field of AI has a notorious record of shifting goalposts whenever something previously thought unattainable is achieved.
> how long would it take for it to start replacing remote contractors and then in-office programmers?
Although I don't think it's possible to replace "programmers", if such scenario does evolve, we would have come up with newer jobs that didn't existed before. Podcasting, Youtuber, UX Designers didn't exist 20 years back. Hard to guess what will come forth.
I would argue that all of research is like that - once something is achieved, people will want to do better things.
After all, it's not an argument.
Until AI can create an Angular application with a .Net Core Azure back-end that meets ever-changing customer requirements ("can we remove the need for Bootstrap 4? Can we make the integration with Active Directory seamless?") on short notice, not very soon at all!
I'm throwing that out there because that's just one of my current projects, but a lot of programmers do things daily that AI simply isn't intended for.
Or college courses, for that matter. Although since you mentioned 10% you probably mean more in the area of research science, which may be a different story.
I think you are arguing for "Not all programming tasks that can be automated away by a bot that can win IOI / ICPC."
However, what I'm asking is: "Does there exist 10% of programming that can be automated away by a bot that can win IOI / ICPC" ?
Furthermore, I think you are also assuming that human programmers remain static, while the AI has to be a 'drop in replacement for humans.' On the other hand, if we look at AWS -- AWS didn't build some AI that is a drop in replacement for sys admin work. AWS built their own API, humans adapted to it.
It seems to me that in a world where such an IOI/ICPC winning bot existed, programmers would adapt to it (just as programmers have adapted to AWS), by figuring out "how can I leverage this API so that I don't have to hire someone to do FOOBAR"
You can see some of the simpler programs that can already be generated on page 12.
Think of eg compilers and interpreters. Thanks to them, perhaps you need only one guy to write software to solve a problem that used to take 10 people: 9 people replaced.
The answer turns out to be pretty boring: As long as humans are still better than machine, humans can provide algorithmic insights and be a source of cheap labels.
So I am pretty pessimistic about this particular task. There are only a small handful of humans in the world who are qualified to help! (according to IMO scores: https://www.imo-official.org/hall.aspx)
Also consider that fact that human IMO contestants have little training in university-level mathematics. The problem setters try to choose problems where knowledge of advanced mathematics doesn't help, in order to produce a level playing field which only measures raw problem-solving ability. But I suspect that postgraduate-level mathematics will nevertheless be useful in programming the AI.
I don't think this is true, as in my experience many of the contestants have already cultured a background in calculus but refrain from using it as the problems are usually designed to actively discourage its use.
Terrence Tao definitely says that doing university math changed his approach to these problems. See https://terrytao.wordpress.com/books/solving-mathematical-pr...
Calculus.
Uni adds a much more axiomatic and formal approach.
There are self learning one and there are one which human to id only.
University math textbooks less so.
Hah, some student solutions take hours to read...
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?
If you give the machine some equations, wouldn't it find a path to the solution pretty fast? Aren't there solvers that aren't considered AI that do that sort of thing?
I did some math contests in school, and a lot of the problems needed some brute force element along with a bit of overview so you didn't waste too much time. Often there'd be a problem that you'd look at and think "hmm this will solve via integration by parts" but the thing was complex enough that you'd potentially screw something up.
I looked in the Gitlab, it seems the problems are already encoded in Lean. Haven't you solved a major part of the problem already if you can formally encode it like that? Half the fun of math contests is getting over the WTF feeling.
Most research papers in Math / Theoretical CS are < 50 pages, while many IMO problems have solutions > 1 page. So it's only a factor of 50 "more complex."
Then, we should be able to encode open problems / conjectures in Math / Theoretical CS into Lean, run this brute fore approach, and have it start auto generating new publications.
To the best of my knowledge, no one has done this yet.
Also, who says that efforts goes up linearly with size?
(Not necessarily agreeing with lordnacho here, just saying that your argument ain't a good one.)
The AMC/AIME/USAMO/IMO set of exams can all be solved without calculus and are not what I'd call "brute force". Perhaps you have experience with a different type of mathematical competition?
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 solvable with school tools. And I'm pretty sure that while you didn't NEED calc and higher subjects, having studied them would give you some edge.
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.
--- 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.)
While you may argue that, for instance, for elementary number theory there are only so many theorems and tricks you can perform, and in fact you can compile such a list right now (which obviously won’t work for combinatorics), brute forcing your way by applying every trick to every degree of freedom of a problem will probably lead you nowhere.