How does this relate to the "IMO Grand Challenge" https://imo-grand-challenge.github.io/ ? Is this a new name / formalization, with prize money attached, or is it entirely independent? (E.g. I see Kevin Buzzard and Leonardo de Moura listed on both that page and at https://aimoprize.com/supporters)
$10M AI Mathematical Olympiad Prize
21–30 of 231 posts
Re: $10M AI Mathematical Olympiad Prize
#22As the parent of a young adult currently half way through their maths undergrad, this kind of fills me with foreboding. I know that proof assistants etc have existed for quite a while now, but what with this and the murmours about OAI's Q* model, I do wonder what will happen to maths as a human endeavour - and as a enabling skill for jobs that can financially support people like my child.
I wouldn't worry. What this means is that mathematics as a skill is going to be back big time, because now you can actually use it everywhere.
Mathematics departments have been closing down for a while now, I think. I think this trend will reverse now. Mathematics itself will change in the process, but for the better.
Re: $10M AI Mathematical Olympiad Prize
#23As the parent of a young adult currently half way through their maths undergrad, this kind of fills me with foreboding. I know that proof assistants etc have existed for quite a while now, but what with this and the murmours about OAI's Q* model, I do wonder what will happen to maths as a human endeavour - and as a enabling skill for jobs that can financially support people like my child.
I wouldn't worry about it. We're going to need humans with specialized mathematical training in the loop.
Besides, these things have a way of surprising us. Before compilers, people wrote machine code by hand. It would have been reasonable to think that compilers would reduce the demand for programmers, but the opposite happened.
Re: $10M AI Mathematical Olympiad Prize
#24As the parent of a young adult currently half way through their maths undergrad, this kind of fills me with foreboding. I know that proof assistants etc have existed for quite a while now, but what with this and the murmours about OAI's Q* model, I do wonder what will happen to maths as a human endeavour - and as a enabling skill for jobs that can financially support people like my child.
I think its pretty clear that in the coming decade intelligence and cognitive labor is going to become very cheap. So your kid should develop some skills outside of that to stay competitive in the job market.
general intelligence will become cheap?
and so your suggestion is to develop skills outside of skills?
Re: $10M AI Mathematical Olympiad Prize
#25It would be cool to have a Patreon-like system for math proofs. But to reward solvers appropriately and at scale, the award conditions and evaluation would have to be very formalized and specific. This seems to be one potential, actually useful application of blockchains which support general purpose computing - if you can port a proof verifier onto them, you give anyone the ability to commit to (and claim) proof bou…
A blockchain provides nothing of value here, what you need is a mechanized proof, and once you have that the blockchain in no way contributes to the trust.
The trust in a Coq proof comes down to "do you believe that the 8kloc kernel faithfully implements CiC+extensions and is this metatheory a sound type system?". As it is today, anyone could claim or commit a proof bounty by posting a Coq / Lean file / project online, all that's required is an email.
Re: $10M AI Mathematical Olympiad Prize
#26I was recently in Palo Alto, and bumped into a newly founded startup (I don't remember the name unfortunately) who set themselves the grand the vision of exactly this: winning a gold medal on the international Olympiad using AI. Their plan was to build mostly on LLMs as a start, and iterate as they go. In their barebones office space, they had a poster with a countdown of the number of weeks till the event: it was 36…
I don't think anything came out of the Netflix prize, did it?
Re: $10M AI Mathematical Olympiad Prize
#27Earlier quoted context omitted.
I think its pretty clear that in the coming decade intelligence and cognitive labor is going to become very cheap. So your kid should develop some skills outside of that to stay competitive in the job market.
Any suggestions?
AI Software Engineering? Baker?
Re: $10M AI Mathematical Olympiad Prize
#28As the parent of a young adult currently half way through their maths undergrad, this kind of fills me with foreboding. I know that proof assistants etc have existed for quite a while now, but what with this and the murmours about OAI's Q* model, I do wonder what will happen to maths as a human endeavour - and as a enabling skill for jobs that can financially support people like my child.
I wouldn't worry. What this means is that mathematics as a skill is going to be back big time, because now you can actually use it everywhere. Mathematics departments have been closing down for a while now, I think. I think this trend will reverse now. Mathematics itself will change in the process, but for the better.
This. Math proofs are useless in 99.99% of situations because they are far too expensive to actually use in production. Only something like AWS would use formal proofs to verify some system property for reliability.
With some super-math Q* bot, a mathematician could presumably create actual proofs/simplifications for complex real world problems/systems at very affordable time and costs (in weeks not years).
The mathematician in this case is far less skilled than the bot, but that doesn't detract from their market value. Most programmers are way less skilled/smart than the library authors that they rely on, that doesn't stop them from earning $$$, because they are useful.
Re: $10M AI Mathematical Olympiad Prize
#29I was recently in Palo Alto, and bumped into a newly founded startup (I don't remember the name unfortunately) who set themselves the grand the vision of exactly this: winning a gold medal on the international Olympiad using AI. Their plan was to build mostly on LLMs as a start, and iterate as they go. In their barebones office space, they had a poster with a countdown of the number of weeks till the event: it was 36…
Well math solving is exactly what the rumored Q* is aiming towards too. I don't think it'll take more than 2 years before some LLM + RL system can take the gold medal. I think companies like OpenAI are aiming for something far more ambitious, like solving a millennium prize problem (even with human assistance). That's the kind of news release that'll add another $100 billion to your market cap.
Their current ambition is to be able to solve school math, which is quite far away from solving unsolved conjectures or math olympiads. I really doubt that any of this is within LLM/transformer scope, except maybe in some auxiliary sense to other, much different architectures.
Re: $10M AI Mathematical Olympiad Prize
#30I was recently in Palo Alto, and bumped into a newly founded startup (I don't remember the name unfortunately) who set themselves the grand the vision of exactly this: winning a gold medal on the international Olympiad using AI. Their plan was to build mostly on LLMs as a start, and iterate as they go. In their barebones office space, they had a poster with a countdown of the number of weeks till the event: it was 36…
I don't think anything came out of the Netflix prize, did it?
I don't think the actual winning algorithm itself was used, because real world systems have more constraints/requirements than what the recommender was trained on. But that was in 2009, pre deep-learning/AI summer, and $1 mil clearly helped stimulate interest in that area.
Today we see multiple billion dollar recommender systems, like Tiktok. Netflix ironically benefits the least from recommenders due to the nature of its dataset (Very expensive, low sample size).