Live data from Hacker News

$10M AI Mathematical Olympiad Prize

aimoprize.com

41–50 of 231 posts

Re: $10M AI Mathematical Olympiad Prize

#41

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

Personally i think markets will be so different from now that this question of where you'll have skills for jobs is less important than asking what will a job mean in 2040. But ok, maybe this is still a minority opinion.

Re: $10M AI Mathematical Olympiad Prize

#42
post #29

Earlier quoted context omitted.

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

AlphaGo solved Go?

Re: $10M AI Mathematical Olympiad Prize

#43
post #25

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…

Sure, any centralized group, ideally a non-profit could run it just as well, and do so without potential complications arising from computation limits.

But they'd have to be entrusted with all the funds, and the financial side may be more difficult to implement. What could be a contract call would involve more real life logistics.

Not to imply that the points or whatever would have to represent anything more than kudos/bragging rights.

It would be interesting to see which problems have the most professional interest, say if every math PhD got 1 million points to commit.

Re: $10M AI Mathematical Olympiad Prize

#44

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.

You do realize that we still learn (and not unnecessarily) addition despite having had calculators for 50+ years?

Math shapes your mind, that’s why we learn it.

Re: $10M AI Mathematical Olympiad Prize

#45
post #21

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 )

The IMO Grand Challenge is "formal to formal" -- a solver is given the problem specified in the Lean programming language, and must produce a solution in Lean. To see more concretely what this setup might look like, check out https://github.com/dwrensha/compfiles.

The AI MO prize is "informal to informal" -- a solver is given a problem in natural language and must produce a solution in natural language.

My belief is that the best way to get to "informal to informal" is to first solve "formal to formal", but not everyone thinks so.

Re: $10M AI Mathematical Olympiad Prize

#46

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

> You can't feasibly host or verify proofs on-chain

I came to the same conclusion with existing systems, full on-chain verification would not be economically feasible.

But perhaps a special-purpose chain specifically made for this may not have the same limitations. Or Truebit-like oracle systems may be possible, where external verifiers can dispute other external verifier's assertions of correctness by running only the (potentially) wrong steps on-chain.

The frontrunning may be avoided by submitting hash(accountid | secret large random number | proof) first, then once that's finalized the full proof with the random number. The random number so the proof can't be brute forced from the hash. Payouts have some reasonable delay so if someone tries to frontrun the second step by intercepting the full proof and submits both steps (possibly with a varied proof) before the second step of the first person is finalized, the first person can still prove with a reference to their first step and their working proof that they were first. This still requires some thought regarding (forced) congestion in relation to the transaction cost and bounty size.

Metamath has the same problem of the system accepting new axioms anywhere, and the same $a statement being used for definitions. I have some hopes for Metamath Zero (https://github.com/digama0/mm0), which is a related system which may be able to fix this.

I think this idea is rather synergistic with proof agents. I think more people would consider developing these if enough bounties were credibly committed. It might speed up and greatly increase the number of formalized proofs.

Re: $10M AI Mathematical Olympiad Prize

#47
post #23

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.

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

I see this reasoning a lot but for me it kinda screams "correlation is not causation". As time passed and technology advanced it was simply more widely used, both on a consumer and business level. Very well may be that if we had to write machine code by hand we would need 10x more developers and a salary of $1kk/year would be average at best.

Do you really think if we get some AI agent that can write a wholly working application based on natural language specification that wouldn't significantly reduce the need for human devs?

Re: $10M AI Mathematical Olympiad Prize

#48
post #6
post #5

Anything you can do with a calculator is obviously trivial. Is there a clear point of departure when AI can no longer handle mathematical reasoning?

The IMO are a bit more involved... e.g. IMO 2023: > Problem 1. Determine all composite integers n > 1 that satisfy the following property: if d1, d2, . . . , dk are all the positive divisors of n with 1 = d1 Although ChatGPT 4 makes a pretty decent start on this already: > To determine all composite integers \( n > 1 \) that satisfy the given property, we need to closely examine the condition set forth: for a composi…

A decent start? It says absolutely nothing about how to solve it, except repeating the question. The part where it tries out the few first numbers is entirely wrong, given that 6 does _not_ satisfy the condition (2 does not divide 3+6=9) and 8 _does_ (2 does divide 4+8=12).

Amusingly, the list of the integers Given that GPT4 is not a model but a full product, behind the scenes it probably coded up and ran a small python code that translated the problem into code, executed it and got its solution for the first few integers. Which would be a good thing to do to start solving a problem like this, except you're not allowed to do that at the IMO, obviously.

Looking at the output of this program, it suggests that powers of primes could be a class of solution (or maybe even the only solutions? I guess that's all the problem was _really_ asking to prove, but having never qualified for the IMO myself, I can't be sure). In fact, for n = p^k, the divisors are [1, p, p^2, ..., p^{k-1}, p^k], and clearly always p^i divides p^{i+1} + p^{i+2} = p^i (p + p^2). I guess this small remark would have gained me a point at the IMO, only 41 to go ;-)

But the other side of the coin is that having those numbers written down in front of you and not even making a conjecture about powers of prime being the answer would really denote poor mathematical reasoning by GPT4. It's only really proving that it can understand what it's being asked, which, I admit, places it in a better position than maybe 90% of the human population, but unfortunately for GPT4 mathematics is the least democratic science of them all - it's always only the top-1 result that matters in the end.

P.S. Being a former mathematician currently working on deep learning, having (or building!) a model that can solve mathematical questions has always been my dream. I'm not even talking about something that can _prove_ things, even just that can understand and rephrase them in different settings (which in mathematics is very, very hard, even for a human). Or spot weaknesses in already stated down proofs. As a graduate student, having something I could chat about to ask silly question while studying a paper would have been a real game changer. Even for best-of-world professionals it would be useful: when the wrong proof about the ABC conjecture came out, it took months of work from the best minds of our world to read through it and disprove it. If Mochizuki had had some tool for automatically checking his proof (and a smaller ego, I guess) he could have caught that early on, saved everybody a lot of work and the whole world some useless drama.

And while we're closer than ever to reaching that, I think GPT4 is still quite a far way from it. But with the pace we've seen recently in AI evolution, who knows...

Re: $10M AI Mathematical Olympiad Prize

#49

Earlier quoted context omitted.

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

AlphaGo solved Go?

"Superhuman at solving" != "solved".

AlphaGo didn't solve go (Ie, can the first mover guarantee a win?). However, it understood go at a far, far superior level to any human.

A mathbot doens't have to solve math in general. It merely has to be better at solving math than any human mathematician to be considered ASI. And it only has to be better than the 'average' human mathematician to be extremely useful in accelerating math research.

Re: $10M AI Mathematical Olympiad Prize

#50

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

Chainlink has solved this. Worth taking a look if you're still interested in this sort of thing.
Post reply on HN