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

31–40 of 231 posts

Re: $10M AI Mathematical Olympiad Prize

#31

Post by dist-epoch »

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…

What's his plan on being allowed to compete?

Or will he be doing it after the fact, when the questions are published.

Re: $10M AI Mathematical Olympiad Prize

#32

Post by Davidzheng »

auggierose wrote: post #22
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.

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.

I don't think it's true that "math departments have been closing for a while now"

Re: $10M AI Mathematical Olympiad Prize

#34

Post by anonylizard »

dimask wrote: post #29
anonylizard wrote: post #17

Earlier quoted context omitted.

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.

Art isn't an easier problem than math. An artbot would have sounded more sci-fi than a mathbot only 2 years ago.

Yet it only took the AI world 1.5 years to go from drawing child scribbles to replicating top artists with like 90% similarity (I can barely tell the difference between AI and human drawn art anymore with the new NovelAI model). It won't be long before AI starts to go superhuman in art skills.

It won't take long from a school-math model to math olympiad model (I'd say 1 year is enough), and going to unsolved conjectures won't be that long either (2-3 years?). We know from AlphaGo that its possible to make AI systems far superhuman at solving some abstract math problem.

Re: $10M AI Mathematical Olympiad Prize

#36

Post by colesantiago »

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…

> This seems to be one potential, actually useful application of blockchain...

No.

Blockchain and anything crypto has absolutely no use case at all other than speculation, please stop suggesting this solution in search of a problem.

Re: $10M AI Mathematical Olympiad Prize

#37

Post by Davidzheng »

slibhb wrote: post #23
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.

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.

It's highly unclear to me what will happen. Probably learning math will be more accessible. But it's unclear how many humans will be involved at the forefront of math research. For example you can imagine a situation where in some parts of math large communities work in a direction guided by a few "visionaries". This sort of thing will not really happen after the commodization of theorem provers. Like instead of an advisor telling a PhD student a problem, they can just plug it in. On the other hand, in some sense the advisor and the student will be equal in the fact that the only thing you will need to do is ask questions?(last part is also speculative)

Re: $10M AI Mathematical Olympiad Prize

#38

Post by machiaweliczny »

singularity2001 wrote: post #7

Maybe the recently announced 1T Parameter Scientific AI will be trained on mathematical papers as well and picks up reasoning on the fly: https://news.ycombinator.com/item?id=38391923 Or at least maybe it will be a good foundation model to be fine-tuned for reasoning?

Picks up reasoning on the fly seems like wishful thinking. On the other hand in nature there also is split into people who get math and those who don’t so maybe there are 2 different ways of bootstrapping brain to be functional and luck is all we need. Anyone knows more on this?

Re: $10M AI Mathematical Olympiad Prize

#39

Post by cottonseed »

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 actually prototyped a system like this, mostly as an exercise to learn about crypto. You can't feasibly host or verify proofs on-chain, so you need external trusted verifiers (e.g. oracles). Making sure the oracles can't front-run proof submission is a challenge. Standard formal proof system (like Lean) are sufficiently expressive, although they weren't built for this and need to be modified to make sure a proof hasn't introduced any additional axioms, as you note. The proof system also becomes a point of attack, so you'd probably want multiple, independent verifiers (which themselves have been formally proved correct). I believe these exist for some proof systems, although I'm not sure about Lean's kernel.

Ultimately, I don't think this is really practical, and investing in AI proof agents is the way to go.

Re: $10M AI Mathematical Olympiad Prize

#40

Post by electrozav »

anonylizard wrote: post #28
auggierose wrote: post #22

Earlier quoted context omitted.

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

There's a massive corpus of useful math proofs, just most of them have been implemented and are second nature now
Post reply on HN