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

151–160 of 231 posts

Re: $10M AI Mathematical Olympiad Prize

#151

Post by jack_riminton »

anonylizard wrote: post #34
dimask wrote: 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…

NovelAI isn't for drawing it's for writing, did you mean something else?

Re: $10M AI Mathematical Olympiad Prize

#152

Post by lupire »

dwrensha wrote: post #147
lupire wrote: post #145

Earlier quoted context omitted.

"Informal to formal" is harder than "formal to formal". These puzzle problems are quite simple (for computers) if you have a formalization. "Informal to informal" is so far snake oil.

> These puzzle problems are quite simple (for computers) if you have a formalization. That may be true someday, but it's not yet! That's exactly what the IMO Grand Challenge is about, and nobody has gotten close to solving it.

Do you have formal problems with formal solutions (so, you know the formalization is sufficiently complete) that cannot be found by existing (powerful) computer search techniques?

Re: $10M AI Mathematical Olympiad Prize

#153

Post by quirino »

haltist wrote: post #94
machiaweliczny wrote: post #38

Earlier quoted context omitted.

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?

It's just a matter of scale because when you add more floating point numbers magical things happen. The magic is called emergence, as in if you have a big enough computer then it can do anything if you prompt it the right way. As a techno-optimist I believe that thinking is simply very complicated arithmetic and by adding enough numbers we can solve any problem.

Depends a lot on how this scales though. If you need 10x as many parameters to get 1% better results for instance, then even if this works it could be impractical.

Re: $10M AI Mathematical Olympiad Prize

#154

Post by Der_Einzige »

pixl97 wrote: post #70
slibhb wrote: post #23

Earlier quoted context omitted.

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.

>There isn’t a rule of economics that says better technology makes more, better jobs for horses. It sounds shockingly dumb to even say that out loud, but swap horses for humans and suddenly people think it sounds about right.

Yes there is actually: https://en.m.wikipedia.org/wiki/Okishio%27s_theorem

Re: $10M AI Mathematical Olympiad Prize

#155

Post by lupire »

7373737373 wrote: post #43
xavxav wrote: post #25

Earlier quoted context omitted.

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

Overhead of block chain is greater than overhead of centralization.

We already have rich math guys like Simons throwing money at people doing math.

Re: $10M AI Mathematical Olympiad Prize

#156

Post by Der_Einzige »

adhocmobility wrote: post #16
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 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.

You speak the truth but people here will hate you for it.

Re: $10M AI Mathematical Olympiad Prize

#157

Post by Der_Einzige »

haltist wrote: post #92
WhitneyLand wrote: post #67

Winning a gold medal here will really be a leap forward for AI creativity and deep insight into problem solving. AI already is already contributing in substantial ways to research. What’s tantalizing here is this next level would take a huge step toward accelerating the pace of advancements in many fields. It will be a milestone in moving past AI being a mere tool in scientific progress to something much greater.

I sense you are a techno-optimist.

Techno optimism is good and should be the default. I wish a16z didn’t ruin that phrase. Techno optimism should evoke Star Trek, not Silicon Valley vibes

Re: $10M AI Mathematical Olympiad Prize

#159

Post by dwrensha »

lupire wrote: post #152
dwrensha wrote: post #147

Earlier quoted context omitted.

> These puzzle problems are quite simple (for computers) if you have a formalization. That may be true someday, but it's not yet! That's exactly what the IMO Grand Challenge is about, and nobody has gotten close to solving it.

Do you have formal problems with formal solutions (so, you know the formalization is sufficiently complete) that cannot be found by existing (powerful) computer search techniques?

About half of the problems in Compfiles have complete solutions. They are marked by the checkmarks in the list at https://dwrensha.github.io/compfiles/index.html .

As far as I know, based on published systems like LeanDojo [1] and Magnushammer [2], computers today can only solve a small handful of the very easiest of these problems (like maybe Imo1959P1).

[1] https://leandojo.org/

[2] https://arxiv.org/abs/2303.04488

Re: $10M AI Mathematical Olympiad Prize

#160

Post by fooker »

Yhippa wrote: post #68

I'm asking this question out of ignorance: if you were able to do this, why would you make it public for $10MM instead of keeping it private and exploiting it. Say, in algorithmic trading models?

Two reasons: (1) These are two different problems. Human mathematicians tend to be good at both, but there's no reason to believe (yet) that this generalization can be achieved with software.

(2) Trading has second order effects, no matter how good your algorithm is, if you apply it at any kind of scale the market reacts to it and you are left with something that doesn't work or cause large losses in the worst case.

Post reply on HN