I'm excited about seeing what the current learning algorithms can do in Math. Games like Chess, Go, Starcraft as "easy" (note the quotes) compared to mathematical theorem proving, and using the bag of tricks (known theorems and axioms) to solve new problems.
Heck, even understanding a problem is a challenge in itself. Just look at the sample question provided:
Let n be an integer greater than or equal to 3. Prove that there is a set of n points in the plane such that the distance between any two points is irrational and each set of three points determines a non-degenerate triangle with rational area.
99.9% of the people would have no idea what to do here.
with AI system it is also hard, you need to have some knowledge graph which would explain what is plane, distance, etc, and map it on some set of axioms, theorems, predicates and functions.
this is what Lean and other theorem provers are trying to build. which would be useful whether you have a human operator generating the proofs or some kind of automated system.
One shouldn't use human concepts for "easy" vs "hard" when applied to AI capabilities. Machines aren't humans. Coal mining is hard for humans, but easy for a Bagger 288. Similarily, computers can do millions of floating point operations per second, where even a single operation would be very hard for humans, especially when larger numbers are involved. Doing the laundry, cleaning the toilet, etc. are all "simple" tasks but we don't have any humanoid robots yet that can do them.
Also important to note: human capabilities are no natural constant. Once you reach human performance in some area, it's not guaranteed that you'll plateau, but instead likely that you'll outstrip human capabilities, especially in areas where there hasn't been billions of years of evolution led engineering like abstract thinking.
>Doing the laundry, cleaning the toilet, etc. are all "simple" tasks but we don't have any humanoid robots yet that can do them.
That's because we have millions of unfortunate underpaid workers on the market with no better options that will do these chores cheaper than it costs to design, build and maintain a robot that can do such things.
Hell, Atlas from Boston Dynamics can already do parkour so I'm sure they can program it to scrub toilets and do laundry but who would buy it for that when the minimum wage is what it is?
The tech is nearly here, the business case isn't until the price comes orders of magnitude down.
Your point about the workers is true, but there are economies of scale here. I don't think it's going to be different in robots than in other areas.
As for the human competition, we often had cases where technology has put humans out of their job. They provide a baseline price that you need to undercut. Today we might use robots to clean nuclear waste sites. Tomorrow we use mass produce them and put them into people's homes. As long as you don't make a larger mess at the toilet than Fukushima you should be fine! :)
Can I prove this by just providing an example? My points are (0,0), (0,sqrt(2)), (sqrt(8),0). This should give irrational side lengths of sqrt(2), sqrt(8), and sqrt(10). The area of this triangle is 2, which is rational.
I solved this by guessing and checking the square roots of positive integers.
The question asks you to prove that it works for every n>=3. So you have to show it works also for n=4, n=5 etc. You are on the right track with square roots though.
Yeah, an alternate phrasing could be "For all integers n >= 3, show that there exists a set of n points in the plane such that the distance between any two points is irrational and each set of three points determines a non-degenerate triangle with rational area."
For only having to find a specific n the phrasing would be something like "Find an integer n >= 3, such that ..."
But in general a good heuristic is that if your solution is really simple odds are you've misunderstood the problem. IMO problems aren't easy. Even the "easy" ones take a bit of work.
Daniel would agree with you that this is an underappreciated and overlooked area of AI research. A 2018 blog post[1] gave an indication that he'd started to turn his attention to this particular area (mathematics) more forcefully.
The difference between being better than humans at simple games and harder games like Go is scale. We thought this wouldn't happen for generations but here we are.
I don't see the how the sorts of problems presented as being qualitatively different as ones we can already solve. The problem is scale and having the problem formally defined. We'll separate the english-to-machine readable form as a separate step as I don't think that's the 'math' part of the challenge--specifically excluding math word problems.
We will develop better representations and search strategies and meta-strategy searching abilities and make advances in improving their runtimes as hardware devices continue to get faster allowing research to accelerate.
For the example question, a machine could have picked a special case, right triangles where a^2 + b^2 = c^2 and the area a*b/2. Now choose a^2, b^2 as whole numbers, say 2 and 3 ==> c = root(5) with area 3.
As noted in other comments, it would then have to take this premise and algebraically extend to all n>3 which I believe we have inductive provers as one example can do.
Huh, was somewhat surprised to see that this uses Lean instead of something purely ML-ful, though I suppose GPT-{2,3} can't be "trusted" to output correct mathematics without something much more rigid to validate it.
A seemingly obvious approach would be to try to get GPT-X to generate candidate proofs and then get a tool like Lean to validate them. Which presumably doesn't work or else I suppose the article would have been about that...
For reference here's a GPT-3 output for the sample question:
Solution:
Suppose the given set of n points is A = (a 1 , a 2 , …, a n ). Between any two points we will draw a line segment connecting them, and let the distance from a 1 to the line segment be d(a 1 ,a 2 ) and d(a 1 ,a 3 ) be the distance from a 1 to the line segment connecting a 2 and a 3.
Since any two of the points determine a line segment connecting them, there are n–2 segments connecting the n–1 points.
Let L be the common perpendicular bisector of two of these segments. So, d(a 1 ,a 2 ) = d(a 1 , L) and d(a 1 ,a 3 ) = d(a 1 , L).
Now, we consider the triangle formed by the points (a 1 , a 2 ) and (a 1 , a 3 ). If we are given the points a 1 , a 2 and a 3 , we can easily find the sides of the triangle.
Since d(a 1 ,a 2 ) + d(a 1 ,a 3 ) = d(a 1 , L) + d(a 1 , L) = 2d(a 1 , L), the triangle formed is right angled and therefore non-degenerate.
We can easily calculate the rational area of such a triangle and the side lengths.
Let us consider the simplest case when n = 3.
We have three points (a 1 , a 2 , a 3 ) such that each of a 1 , a 2 and a 3 are different.
Therefore, we can form a triangle by connecting a 1 , a 2
Always fun to grade these kinds of proofs with a bottle of wine at 2am.
I never faulted anyone for doing this, but I sometimes wondered why they bothered. Throwing stuff to a wall to see what sticks doesn't give you points.
One of my math professors had a "BS" stamp for things like this. If it were worth X points, you'd lose X-5 when it was so obviously a rambling mess. He'd rather you just say "I don't know" than waste both your time and his. Perhaps that's just an advantage of tenure, though.
The actual article title is "At the Math Olympiad, Computers Prepare to Go for the Gold" which also has the advantage of fitting the HN length requirement without a dangling "To".
> IMO problems are simple, but only in the sense that they don’t require any advanced math — even calculus is considered beyond the scope of the competition.
I kind of disagree. IMO problems require a lot of studying and theory that an average person wont know.
"and each set of three points determines a non-degenerate triangle with rational area" <- that's not language I knew in elementary school. Just being able to read what the question wants is a skill that isn't available to most elementary students.
I understand that, but elementary quantum physics is still grossly past the level of the students and required more advanced theory just to get to that elementary level understanding of the subject.
Well, maybe not elementary school, but in highschool you should encounter those, especially second part. Non-degenerate in that case is fancy word for saying that those point cannot form a line (or a single point) - just that triangle is actually a triangle.
This is pretty common term when it comes to math Olympiad so in would be extremely unlikely that someone can get to imo without encountering that in the past during training
In practice, yeah, "an average person" wouldn't know where to begin. And a brilliant high schooler who hasn't studied maths beyond the high-school curriculum won't ace the test. Though he could get a medal, particularly if the geometry and combinatorics questions are friendly.
But the conceit of the IMO has always been that the problems are drawn from a very limited selection of fields, which are/were commonly taught in high schools around the world. No need for complex numbers, calculus, abstract algebra, or trigonometry (though any of these may end up used in an alternative solution).
They show up in a few other areas, like probabilistic analysis of algorithms or sketching (e.g. Chernoff bounds and definitely the Cauchy-Schwartz ineq.). But you're right, nothing heavyweight like Muirheads has many applications.
But a surprising number of them can be solved with the insight only that x^2 >= 0. (Both Cauchy-Schwartz and AM/GM reduce to that if you squint hard enough). And that's accessible to any maths student.
IMO problems are designed such that an average (ok, maybe slightly-above average) person can follow the solution, but it takes skill to come up with it in the first place. Just like calculus is standard curriculum for hundreds of thousands of high school students around the world, but we still think Isaac Newton and Gottfried Leibniz were genii for coming up with it.
Yeah, they do often require a lot of math. It's just a restricted set of topics. The IMO doesn't do any calculus or anything beyond calculus like real analysis, topology, etc. It does have a lot of geometry problems that use geometry that typically isn't in the American curriculum, and it has topics like number theory that aren't really in a standard high school curriculum either. But the topics are restricted so that they are pretty close to understandable by someone who has just done well in a standard high school mathematics curriculum.
Here's an example. For the problem they include in the article:
Let n be an integer greater than or equal to 3. Prove that there is a set of n points in the plane such that the distance between any two points is irrational and each set of three points determines a non-degenerate triangle with rational area.
This is a whole lot easier if you're familiar with Pick's Theorem, which gives you a formula for the area of a polygon whose corners are integer lattice points. In particular, any three integer lattice points define a triangle with rational area. So all you have to do is find n points that aren't colinear with each other and have irrational distance, and you'll solve the problem.
Technically, you could do this without Pick's Theorem, because you'll be able to find an equivalent formula for the area of these triangles. But it's much easier if you do know Pick's Theorem, and that's the sort of thing that you typically don't pick up in standard high school math, but you would pick up if you were practicing a bunch of different Olympiad-type problems.
Ha, Pick's theorem. Such hopelessly advanced problems (I'll give an example shortly) are well beyond what a cluster of ten thousand GPU's can solve today if trained for a thousand days on the types of math you've mentioned and then given a hundred hours to compute the answer to an infinitely, staggeringly and mind-bendingly intricate problem such as this one:
"Starting at 2, how many times must you double the number for the result to exceed 10?".
(Or a similarly trivial one.) Yeah. Really. Try it. They don't understand language at all. Just try to interact with any of the assistant or computational knowledge engines.
Here's what wolfram alpha gives you for that query:
Query:
Starting at 2, how many times must you double the number for the result to exceed 10?
Computed response:
1 | adjective | (especially of eyes) bulging or protruding as with fear
2 | adjective | appropriate to the beginning or start of an event
3 | noun | a turn to be a starter (in a game at the beginning)
For the challenge, they give the AI a formal representation of the problem in Lean. To remove ambiguity about the scoring rules, we propose the formal-to-formal (F2F) variant of the IMO: the AI receives a formal representation of the problem (in the Lean Theorem Prover), and is required to emit a formal (i.e. machine-checkable) proof. We are working on a proposal for encoding IMO problems in Lean and will seek broad consensus on the protocol.
So far it's pretty much mechanical∗. The big question is how you will formalize Area(p1, p2, p3). Heron's could possibly make the problem much harder than cross product.
An AI that can do well on the IMO can likely also be useful when applied to actual problems in mathematics. Also, calling the "IMO" an "glorified rat race" is fairly demeaning to those that compete in it.
I have no doubt that we are not far away from winning an IMO gold medal with an AI algorithm. I am not so sure it will come from the lean-team though. There are more people working in the direction, with varying focus on the AI or the automated prover aspect of things.
I have the suspicion that AI-mathematicians will be foremost AI, and only secondary theorem provers. This is because what is mentioned in the article, mathematicians first look for patterns in these questions, and then apply their toolset to them. Only the final step is what theorem provers are currently good in.
But, only time will tell which team will make it first to the finish line.
FTA: “For example, one of the oldest results in math is Euclid’s proof from 300 BCE that there are infinitely many prime numbers. It begins with the recognition that you can always find a new prime by multiplying all known primes and adding 1”
So, if all the primes you know are 5 and 7, you can find a new one by computing 5×7+1? ;-)
This is a very common error. The claim doesn’t even hold if you know the first n primes. The first counterexample is 2×3×5×7×11×13+1=59×509. All you can tell is that the result has at least one prime factor that’s not yet in your list.
It's true that's a common error, but if we're going to be really pedantic: the article doesn't say that multiplying all known primes and adding 1 results in a prime number, it says it's a way to find a new prime. (In fact, all of the result's prime factors are primes that weren't in the list you started with.)
Picking a random number isn't guaranteed to help you find a prime number. However, doing the "take all the prime numbers and multiply them and add 1" always produces at least one prime number; either the result or the factors of the number.
Here's a slightly more rigorous version of the proof for anyone interested:
1. Suppose the list of primes is finite, and that they are P_1, P_2, P_3 .., P_n
2. Consider the new number P_1 * P_2 * P_3 * .. * P_n + 1. None of the P_is divide this number. Therefore, by definition, it it is a prime.
3. The number we found in (2) is not any of the P_is, and it is a prime. This contradicts the assumption we made in (1). So, the assumption in (1) is wrong, there must be infinitely many primes
The examples in parent's post do not work because they do not follow the framework of this proof. I see parent's point that the claim in the article isn't technically correct, but I think it's reasonable to allow some handwaving in an accessible article written in English :-)
I seem to be associated with that quote (and of course I didn't say it -- indeed when I spoke to Quanta I used factorials plus one). When the article appeared I emailed Kevin Hartnett immediately to suggest replacing that line with something like "...using 1 plus the product of all known primes" but he seemed to be happy with what he'd written -- his argument was that what he wrote was ambiguous but not definitely wrong.
One of the founders of the IMO Grand Challenge here. FYI I presented the challenge along with a preliminary roadmap at AITP 2020 last week: https://youtu.be/GtAo8wqWHHg. No way to know if gold is five years out or five hundred but I hope the challenge spurs progress in the field either way.
68 comments
[ 2.8 ms ] story [ 147 ms ] threadHeck, even understanding a problem is a challenge in itself. Just look at the sample question provided:
Let n be an integer greater than or equal to 3. Prove that there is a set of n points in the plane such that the distance between any two points is irrational and each set of three points determines a non-degenerate triangle with rational area.
99.9% of the people would have no idea what to do here.
Also important to note: human capabilities are no natural constant. Once you reach human performance in some area, it's not guaranteed that you'll plateau, but instead likely that you'll outstrip human capabilities, especially in areas where there hasn't been billions of years of evolution led engineering like abstract thinking.
That's because we have millions of unfortunate underpaid workers on the market with no better options that will do these chores cheaper than it costs to design, build and maintain a robot that can do such things.
Hell, Atlas from Boston Dynamics can already do parkour so I'm sure they can program it to scrub toilets and do laundry but who would buy it for that when the minimum wage is what it is?
The tech is nearly here, the business case isn't until the price comes orders of magnitude down.
Your point about the workers is true, but there are economies of scale here. I don't think it's going to be different in robots than in other areas.
As for the human competition, we often had cases where technology has put humans out of their job. They provide a baseline price that you need to undercut. Today we might use robots to clean nuclear waste sites. Tomorrow we use mass produce them and put them into people's homes. As long as you don't make a larger mess at the toilet than Fukushima you should be fine! :)
Can I prove this by just providing an example? My points are (0,0), (0,sqrt(2)), (sqrt(8),0). This should give irrational side lengths of sqrt(2), sqrt(8), and sqrt(10). The area of this triangle is 2, which is rational.
I solved this by guessing and checking the square roots of positive integers.
For only having to find a specific n the phrasing would be something like "Find an integer n >= 3, such that ..."
But in general a good heuristic is that if your solution is really simple odds are you've misunderstood the problem. IMO problems aren't easy. Even the "easy" ones take a bit of work.
[1] https://dselsam.github.io/posts/2018-06-24-mathematics-our-o...
I don't see the how the sorts of problems presented as being qualitatively different as ones we can already solve. The problem is scale and having the problem formally defined. We'll separate the english-to-machine readable form as a separate step as I don't think that's the 'math' part of the challenge--specifically excluding math word problems.
We will develop better representations and search strategies and meta-strategy searching abilities and make advances in improving their runtimes as hardware devices continue to get faster allowing research to accelerate.
For the example question, a machine could have picked a special case, right triangles where a^2 + b^2 = c^2 and the area a*b/2. Now choose a^2, b^2 as whole numbers, say 2 and 3 ==> c = root(5) with area 3.
As noted in other comments, it would then have to take this premise and algebraically extend to all n>3 which I believe we have inductive provers as one example can do.
Solution:
Suppose the given set of n points is A = (a 1 , a 2 , …, a n ). Between any two points we will draw a line segment connecting them, and let the distance from a 1 to the line segment be d(a 1 ,a 2 ) and d(a 1 ,a 3 ) be the distance from a 1 to the line segment connecting a 2 and a 3.
Since any two of the points determine a line segment connecting them, there are n–2 segments connecting the n–1 points.
Let L be the common perpendicular bisector of two of these segments. So, d(a 1 ,a 2 ) = d(a 1 , L) and d(a 1 ,a 3 ) = d(a 1 , L).
Now, we consider the triangle formed by the points (a 1 , a 2 ) and (a 1 , a 3 ). If we are given the points a 1 , a 2 and a 3 , we can easily find the sides of the triangle.
Since d(a 1 ,a 2 ) + d(a 1 ,a 3 ) = d(a 1 , L) + d(a 1 , L) = 2d(a 1 , L), the triangle formed is right angled and therefore non-degenerate.
We can easily calculate the rational area of such a triangle and the side lengths.
Let us consider the simplest case when n = 3.
We have three points (a 1 , a 2 , a 3 ) such that each of a 1 , a 2 and a 3 are different.
Therefore, we can form a triangle by connecting a 1 , a 2
I never faulted anyone for doing this, but I sometimes wondered why they bothered. Throwing stuff to a wall to see what sticks doesn't give you points.
I assume it's not mentioned in OP because GPT-f came out too recently for them to interview or profile compared to this Lean-using team.
I kind of disagree. IMO problems require a lot of studying and theory that an average person wont know.
But the conceit of the IMO has always been that the problems are drawn from a very limited selection of fields, which are/were commonly taught in high schools around the world. No need for complex numbers, calculus, abstract algebra, or trigonometry (though any of these may end up used in an alternative solution).
Here's an example. For the problem they include in the article:
Let n be an integer greater than or equal to 3. Prove that there is a set of n points in the plane such that the distance between any two points is irrational and each set of three points determines a non-degenerate triangle with rational area.
This is a whole lot easier if you're familiar with Pick's Theorem, which gives you a formula for the area of a polygon whose corners are integer lattice points. In particular, any three integer lattice points define a triangle with rational area. So all you have to do is find n points that aren't colinear with each other and have irrational distance, and you'll solve the problem.
Technically, you could do this without Pick's Theorem, because you'll be able to find an equivalent formula for the area of these triangles. But it's much easier if you do know Pick's Theorem, and that's the sort of thing that you typically don't pick up in standard high school math, but you would pick up if you were practicing a bunch of different Olympiad-type problems.
"Starting at 2, how many times must you double the number for the result to exceed 10?".
(Or a similarly trivial one.) Yeah. Really. Try it. They don't understand language at all. Just try to interact with any of the assistant or computational knowledge engines.
Here's what wolfram alpha gives you for that query:
Query:
Starting at 2, how many times must you double the number for the result to exceed 10?
Computed response:
1 | adjective | (especially of eyes) bulging or protruding as with fear 2 | adjective | appropriate to the beginning or start of an event 3 | noun | a turn to be a starter (in a game at the beginning)
For the challenge, they give the AI a formal representation of the problem in Lean. To remove ambiguity about the scoring rules, we propose the formal-to-formal (F2F) variant of the IMO: the AI receives a formal representation of the problem (in the Lean Theorem Prover), and is required to emit a formal (i.e. machine-checkable) proof. We are working on a proposal for encoding IMO problems in Lean and will seek broad consensus on the protocol.
So far it's pretty much mechanical∗. The big question is how you will formalize Area(p1, p2, p3). Heron's could possibly make the problem much harder than cross product.
∗Although I may have made some or many mistakes.
Also I can't find an accompanying dataset from the link: https://imo-grand-challenge.github.io/
EDIT: Nvm found it: https://github.com/IMO-grand-challenge/formal-encoding/blob/.... But there are only a handful of formal encodings of problems and last commit was from a year ago!
As such, they are somewhat low-hanging fruits for the AI field, but I wouldn't say that I'd found that impressive or game changing in any way.
I have the suspicion that AI-mathematicians will be foremost AI, and only secondary theorem provers. This is because what is mentioned in the article, mathematicians first look for patterns in these questions, and then apply their toolset to them. Only the final step is what theorem provers are currently good in.
But, only time will tell which team will make it first to the finish line.
So, if all the primes you know are 5 and 7, you can find a new one by computing 5×7+1? ;-)
This is a very common error. The claim doesn’t even hold if you know the first n primes. The first counterexample is 2×3×5×7×11×13+1=59×509. All you can tell is that the result has at least one prime factor that’s not yet in your list.
But yes, the all part is a good way of being pedantic.
1. Suppose the list of primes is finite, and that they are P_1, P_2, P_3 .., P_n
2. Consider the new number P_1 * P_2 * P_3 * .. * P_n + 1. None of the P_is divide this number. Therefore, by definition, it it is a prime.
3. The number we found in (2) is not any of the P_is, and it is a prime. This contradicts the assumption we made in (1). So, the assumption in (1) is wrong, there must be infinitely many primes
The examples in parent's post do not work because they do not follow the framework of this proof. I see parent's point that the claim in the article isn't technically correct, but I think it's reasonable to allow some handwaving in an accessible article written in English :-)