Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

$10M AI Mathematical Olympiad Prize

aimoprize.com

Post reply on HN
Print view View original

121–130 of 231 posts

Re: $10M AI Mathematical Olympiad Prize

#121

Post by haltist »

WhitneyLand wrote: post #110
haltist wrote: post #92

Earlier quoted context omitted.

I sense you are a techno-optimist.

Maybe somewhat, but is anything I said that much of a leap? Do you consider AI to have already considered substantially to the advancement of science? For example AlphaFold, Weather forecasting, Algorithm optimization, etc

I believe the universe is a computer executing an algorithm. In fact, the universe is AI. This is a common belief among many techno-optimist church goers. People themselves are basically just numbers, aka algorithms, so future AI/numbers (people) will definitely contribute to scientific progress.

Re: $10M AI Mathematical Olympiad Prize

#122

Post by killerstorm »

daxfohl wrote: post #101

I'd still call this fancy autocomplete. I imagine the jump from this, to "come up with an interesting new branch of math to explore", is a long way off.

By that definition 99.99% people are also fancy autocomplete.

How many people you know who came up with an interesting new branch of math?

Re: $10M AI Mathematical Olympiad Prize

#123

Post by andyjohnson0 »

daxfohl wrote: post #95
andyjohnson0 wrote: post #15

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

In a way, all math proofs already exist. Humans just have to determine what is worth looking for and uncover them. AI will help us do the latter. But we still have to do the former ourselves. It will still require sound mathematical knowledge and understanding, to know what are the interesting questions to ask. Even if AI knows all the answers, it doesn't change anything because the answers already exist anyway.

That kind of Platonism also implies that all possible computer programs already exist: because any program is merely a very large natural number, the set of which has infinite cardinality. I'm not sure how helpful this is for the practice of humans doing mathematics or software development though.

Re: $10M AI Mathematical Olympiad Prize

#124

Post by quirino »

dooglius wrote: post #115

Seems better to go by AIME-style scoring (explicit 3-digit number answer) otherwise there's the question of whether an AI really solved the problem or just bullshitted enough relevant keywords to get partial credit.

IMO is competitive enough you can't bullshit your way to a gold medal

Re: $10M AI Mathematical Olympiad Prize

#125

Post by eddtries »

anonylizard wrote: post #17
gregdoesit wrote: post #2

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

I have a couple friends who did the Math tripos at Cambridge (so a pretty high level!) who work in tech and have unanimously said they have 0% expectations of an LLM doing a millennium problem anytime soon

Re: $10M AI Mathematical Olympiad Prize

#126

Post by esafak »

daxfohl wrote: post #101

I'd still call this fancy autocomplete. I imagine the jump from this, to "come up with an interesting new branch of math to explore", is a long way off.

Fancy autocomplete is made possible by understanding.

Can you imagine correctly autocompleting a proof to a Millennium Prize problem any other way?

Re: $10M AI Mathematical Olympiad Prize

#127

Post by eddtries »

alecco wrote: post #86
gregdoesit wrote: post #2

I 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 wish there was a serious study of Dunning-Kruger effect in Silicon Valley.

And HN!

Re: $10M AI Mathematical Olympiad Prize

#128

Post by [deleted] »

andyjohnson0 wrote: post #15

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

[deleted]

Re: $10M AI Mathematical Olympiad Prize

#129

Post by eddtries »

xavxav wrote: post #25
7373737373 wrote: post #11

It 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 onlin…

First person to submit a mechanised proof gets the payout to the address that submits the code? People can pool money into a pot? No one manages the funds individually and on a set date funds return to senders?

Re: $10M AI Mathematical Olympiad Prize

#130

Post by eddtries »

baq wrote: post #89
7373737373 wrote: post #11

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

I don't think you need the blockchain to post a verifiable, cryptographically signed proof of any theorem. A simple email is good enough for that. Blockchains are append-only databases, sometimes (usually?) with 'slow' thrown in somewhere.

First person to submit a mechanised proof gets the payout to the address that submits the code? People can pool money into a pot? No one manages the funds individually and on a set date funds return to senders?

That’s an app on top of the append only DB with some logic that either requires IRL groups to manage it, or a blockchain contract. I prefer the latter tbh!

Post reply on HN