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

201–210 of 231 posts

Re: $10M AI Mathematical Olympiad Prize

#201

Post by govg »

openquery wrote: post #116

Can automated theorem provers solve mathematical olympiad problems in a reasonable time given enough compute? LLMs are quite good at generating semantically correct language. I remember reading a paper about extending the planning capabilities of GPT-4 by using a Planning Domain Definition Language [0]. By that same logic could an LLM not translate the olympiad problem into a form suitable for a theorem prover? [0] h…

https://imo-grand-challenge.github.io/

This is a similar contest where the plan is exactly as you describe - to develop a way to solve formal descriptions in Lean of IMO problem.

Re: $10M AI Mathematical Olympiad Prize

#204

Post by EVa5I7bHFq9mnYK »

auntienomen wrote: post #197
EVa5I7bHFq9mnYK wrote: post #195

Earlier quoted context omitted.

We can look at it this way: there are ~1000 chess Grandmasters and one World Champion. It took very short time for AI to go from beating an average GM to beating World Champion. There are ~1000 MO winners and 1 (one) Millenial problem solver ...

We can. But doing so frames math research as the same sort of activity as math problem solving.. it's not. Many imo champions struggle to do any successful math research. And many successful math researchers (e.g., all of the most recent batch of Fields medallists) never did the Oympiad at all.

Yet the one and only Millenial problem solver was a MO winner too, so there is some overlap.

Re: $10M AI Mathematical Olympiad Prize

#205

Post by govg »

Yhippa wrote: post #194
BeetleB wrote: post #109

Earlier quoted context omitted.

I see no reason to believe such a machine would be helpful for algorithmic trading. Why should it? How well do current gold medalists do in trading?

I was curious as to why an algorithmic trading firm is sponsoring this. What's in it for them?

A lot of finance companies sponsor events / prizes like this simply as a means of advertising and PR. If you come across this prize as a math student, now XTX is in your head and maybe you'll look them up and decide to intern there. And 10m is a drop in the bucket for such goodwill and PR, especially because anyone who has the skills to win this can surely be hired and make them as much money.

Re: $10M AI Mathematical Olympiad Prize

#206

Post by auntienomen »

paulddraper wrote: post #199
Enginerrrd wrote: post #132

Earlier quoted context omitted.

Yeah, millennium problems almost certainly require truly novel nontrivial ideas to solve. That's a tough thing for AI to do. On the other hand, Terrence Tao had an interesting article on his blog a while back where he was trying to solve a problem and asked chatGPT about it in a high-level strategy sense. ChatGPT suggested several reasonable approaches, one of which turned out to work. That's nowhere near solving a m…

Ask yourself what mathematicians do today... They decompose problems, solve specialized subsets, examine more general cases, use existing proofs, do some numerical analysis, etc.

Yeah, but none of that gets you a solution to a Millennium problem. One needs an AI to do something like what Peter Scholze did in inventing perfectoid spaces or Perelman in introducing his entropy function. You can treat axiom invention as a game, I suppose, but the space of possible moves is uhh rather large.

Re: $10M AI Mathematical Olympiad Prize

#207

Post by auntienomen »

EVa5I7bHFq9mnYK wrote: post #204
auntienomen wrote: post #197

Earlier quoted context omitted.

We can. But doing so frames math research as the same sort of activity as math problem solving.. it's not. Many imo champions struggle to do any successful math research. And many successful math researchers (e.g., all of the most recent batch of Fields medallists) never did the Oympiad at all.

Yet the one and only Millenial problem solver was a MO winner too, so there is some overlap.

Sample size 1.

Here's what Andrew Wiles, the only other person to have solved a Millennium-class problem has to say of math competition: "Let me stress that creating new mathematics is a quite different occupation from solving problems in a contest. Why is this? Because you don't know for sure what you are trying to prove or indeed whether it is true."

Re: $10M AI Mathematical Olympiad Prize

#208

Post by Imnimo »

It feels like 10M is a fraction of what it would cost to train such a model. Even if we assume an eventual winner would be willing to release the model and forgo potential profits, does this prize really motivate development if it doesn't even cover costs?

Re: $10M AI Mathematical Olympiad Prize

#209

Post by EVa5I7bHFq9mnYK »

auntienomen wrote: post #207
EVa5I7bHFq9mnYK wrote: post #204

Earlier quoted context omitted.

Yet the one and only Millenial problem solver was a MO winner too, so there is some overlap.

Sample size 1. Here's what Andrew Wiles, the only other person to have solved a Millennium-class problem has to say of math competition: "Let me stress that creating new mathematics is a quite different occupation from solving problems in a contest. Why is this? Because you don't know for sure what you are trying to prove or indeed whether it is true."

Sample size > 1 for sure, Terence Tao comes to mind, as well as Dr. Maryam Mirzakhani.

Nobody argues it's the same, after all MO problems are designed to be solved in ~an hour, but we are talking about mental capabilities.

Re: $10M AI Mathematical Olympiad Prize

#210

Post by sdwr »

disgruntledphd2 wrote: post #111
larodi wrote: post #91

Earlier quoted context omitted.

Well this thing about fingers, etc in drawings. Lets put it this way - for us mere mortals the generative images look very much okay. To artists and people who actually draw something, well ... they very often spot inconsistencies in the whole production, including how fingers, arms, overall body posture, etc is presented. So it is exactly what we can expect - good enough on average, but actually a mediocre result of…

It's a weighted average over the prompts and data. Mediocrity is exactly what we'd expect from such an approach. Now, if we end up seeing mastery, that would be extremely interesting.

This is a very mediocre understanding of deep learning :)
Post reply on HN