18 ms·

$10M AI Mathematical Olympiad Prize

281 points by jasondavies 3y ago

dwrensha 3y ago
> $5mn will be awarded to the first publicly-shared AI model Thank for you the emphasis on openness!
supergirl 3y ago
not sure there is much point to this. currently no model is even at the level of primary school math. it will take decades until it can win a gold medal in maths. it won't happen overnight. it will happen slowly. will they still give out the prize in 20 years from now, when it won't seem like such a breakthrough?
up2isomorphism 3y ago
What is fundamentally different about solving IMO compared to solve any other math problems in AI sense?
userforcomment 3y ago
Great marketing stunt, nice work by XTX HR!
gregdoesit 3y ago
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 at the time. It sounded interesting to wonder how far they could go with this kind of approach. I thought they were aiming for the moon: but also respected the boldness and determination. They had the funding to operate for at least a year, and were very focused to get there. Seems like this prize will supr hundreds (or thousands) of teams competing in exactly this space. Perhaps it will have a similar effect like the $1M Netflix Prize in 2009 for recommendations algorithms!
- mlengineerio 3y ago
  Can you share the name of the startup? I'm also in Palo Alto and tinkering LLM for Match competition too (math.llmlab.io).
- anonylizard 3y ago
  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.
  - dimask 3y ago
    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.
    - anonylizard 3y ago
      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.
      - RandomLensman 3y ago
        AlphaGo solved Go?
arcza 3y ago
Of course XTX is sponsoring this
rvz 3y ago
Great, a worthy competition which being first and correctness completely matter and may the best AI model win. Hopefully DeepMind doesn’t enter otherwise they would smoke everyone else other than OpenAI. Speaking of which, I’ll give you a 1% chance of winning with this paper from OpenAI: [0] with the MATH dataset: [1] EDIT: Why the downvotes? I'm trying to help you here and give you a starting point to win the competition? What's wrong with helping others? [0] https://arxiv.org/abs/2305.20050 https://arxiv.org/abs/2305.20050 [1] https://github.com/hendrycks/math https://github.com/hendrycks/math
daoboy 3y ago
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?
- devit 3y ago
  It's problem solving (i.e. finding a proof of a statement or finding one or more mathematical objects that have some given properties and proving they have them and possibly that no other objects do), not computation.
  - daoboy 3y ago
    That distinction seems really obvious now that you said it. Thank you.
- edf13 3y ago
  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 < d2 < · · · < dk = n, then di divides di+1 + di+2 for every 1 ⩽ i ⩽ k − 2 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 composite number $ n $ with its divisors $ d_1, d_2, \ldots, d_k $ where $ 1 = d_1 < d_2 < \cdots < d_k = n $, the property $ d_i $ divides $ d_{i+1} + d_{i+2} $ must hold for every $ 1 \leq i \leq k - 2 $. Let's break down the problem: 1. *Composite Number Requirement*: We are looking for composite numbers, which are integers greater than 1 that are not prime. These numbers have more than two distinct positive divisors. 2. *Divisor Property*: The property $ d_i | (d_{i+1} + d_{i+2}) $ means that $ d_{i+1} + d_{i+2} $ is a multiple of $ d_i $. 3. *Systematic Examination*: We will analyze this property systematically for composite numbers starting from the smallest composite number (4) and going upwards. Let's start the analysis: - For $ n = 4 $, the divisors are $ 1, 2, 4 $. Here, $ 1 | (2 + 4) $, so 4 satisfies the condition. - For $ n = 6 $, the divisors are $ 1, 2, 3, 6 $. Here, $ 1 | (2 + 3) $ and $ 2 | (3 + 6) $, so 6 satisfies the condition. - For $ n = 8 $, the divisors are $ 1, 2, 4, 8 $. Here, $ 1 | (2 + 4) $, but $ 2 \nmid (4 + 8) $, so 8 does not satisfy the condition. Let's implement a systematic method to identify such composite numbers up to a reasonable limit (let's say up to 100 for a start) and check if they satisfy the given condition. The composite integers greater than 1 and up to 100 that satisfy the given property are: 4, 8, 9, 16, 25, 27, 32, 49, 64, and 81. Each of these numbers has the characteristic that for all their positive divisors $ d_1, d_2, \ldots, d_k $ (where $ 1 = d_1 < d_2 < \cdots < d_k = n $), the condition $ d_i $ divides $ d_{i+1} + d_{i+2} $ is true for every $ 1 \leq i \leq k - 2 $.
singularity2001 3y ago
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 https://news.ycombinator.com/item?id=38391923 Or at least maybe it will be a good foundation model to be fine-tuned for reasoning?
- machiaweliczny 3y ago
  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?
  - haltist 3y ago
    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.
    - quirino 3y ago
      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.
      - haltist 3y ago
        You gotta be more techno-optimistic. People are just arithmetic and an existence proof that algorithms can be intelligent. People are just math so it's obviously possible to engineer general artififial intelligence with just math and computers. It's all a matter of adding up the right floating point numbers in the right (partial) order (modulo parallelism).
      - 3y ago
7373737373 3y ago
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 bounties. Now, precisely formalizing specific conjectures and ensuring the proof system is expressive enough but doesn't allow for the introduction of any new assumptions is another problem...
- xavxav 3y ago
  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 online, all that's required is an email.
  - 7373737373 3y ago
    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.
    - lupire 3y ago
      Overhead of block chain is greater than overhead of centralization. We already have rich math guys like Simons throwing money at people doing math.
  - eddtries 3y ago
andyjohnson0 3y ago
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.
- adhocmobility 3y ago
  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.
  - RugnirViking 3y ago
    general intelligence will become cheap? and so your suggestion is to develop skills outside of skills?
  - nickfromseattle 3y ago
    Any suggestions?
    - therealdrag0 3y ago
      Plumber
    - airstrike 3y ago
      AI Software Engineering? Baker?
    - realharo 3y ago
      Stockpile metals and rare earth elements. Natural resources will be the beginning and the end of trade. (not actually serious, at least not yet)
  - Davidzheng 3y ago
    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.
svat 3y ago
How does this relate to the "IMO Grand Challenge" https://imo-grand-challenge.github.io/ 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 https://aimoprize.com/supporters)
- svat 3y ago
  Answering my own question: Alex Gerko (who's behind the $10M prize here) says: > "It came about as me checking on the status of IMO Grand Challenge (which was launched in 2019 https://imo-grand-challenge.github.io https://imo-grand-challenge.github.io) and deciding that it's time to give this idea a boost" https://twitter.com/AlexanderGerko/status/1729207936625627336 https://twitter.com/AlexanderGerko/status/172920793662562733...
- dwrensha 3y ago
  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 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.
  - lupire 3y ago
    "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.
    - dwrensha 3y ago
      > 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.
aaron695 3y ago
[dead]
WhitneyLand 3y ago
Before gold at the math Olympiad, it would be nice if GPT 4 could merely evaluate an expression like this into an exact solution : 3 + 1 / (3 + 1 / (3 + 1/3))
- dmd 3y ago
  Works for me... https://cloud.typingmind.com/share/29d28743-b6a7-4716-b1aa-a2f03bce16eb https://cloud.typingmind.com/share/29d28743-b6a7-4716-b1aa-a...
  - WhitneyLand 3y ago
    That’s helpful thank you. Would you mind trying it 4 times and tell how many succeed? I see it work occasionally but seems <= 50% success rate. See here: https://chat.openai.com/share/6da22a7b-b8f8-4611-b5f7-38048f3414e0 https://chat.openai.com/share/6da22a7b-b8f8-4611-b5f7-38048f...
    - dmd 3y ago
      Worked 6/6 times for me.
      - WhitneyLand 3y ago
        Bizarre, I don’t see how this could be chance. I’m using mostly the ChatGpt client with GPT-4 and no special instructions. Maybe you’re using a model variation via the public API?
        dmd 3y ago
        I’m using gpt-4-turbo
haltist 3y ago
We will solve math with math and this project will succeed as foretold by prophets of techno-optimism like Marc Andreesen, Elon Musk, and Bill Gates. All we need is the right architecture, aka mathematical formula for giving all of math a smooth manifold structure. How this works for discrete structures like integers is left as an exercise for the reader and future AI which will figure out how to improve themselves and deal with discrete and non-smooth mathematical problems. I can win this challenge by the way for $80B. I already know what architecture is required to solve math with math but I need the money to buy the GPUs. You might think such a recursive application of math is logically circular but it is not and all I need is $80B to prove it (pun intended). Claude did not like this comment at all, ironically: I do not have enough context to fully evaluate those claims or determine if that approach would work. Solving all of mathematics is an extraordinarily ambitious goal that would require fundamental theoretical advances we do not yet possess. While future AI systems may someday make significant progress on longstanding mathematical problems, making definitive claims about solutions requires rigorous mathematical proof and analysis beyond optimistic speculation. I'd encourage focusing discussion on specific mathematical questions or areas of research rather than making broad, unsupported assertions about solving all of mathematics.
WhitneyLand 3y ago
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.
- haltist 3y ago
  I sense you are a techno-optimist.
  - WhitneyLand 3y ago
    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
    - haltist 3y ago
      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.
      - ShamelessC 3y ago
        Are you serious? edit: you’re either trolling or mentally ill. If it’s the latter, I sincerely apologize. Hope things get better for you soon. edit edit: I saw your comments about the art project. Thank God. I didn’t want to live in a world where someone like that existed.
        deleted 3y ago
        [deleted]
Yhippa 3y ago
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?
- nathanfig 3y ago
  Some private enterprises would undoubtedly ignore this prize, but a lot of academic researchers (including students) would be more than motivated by this prize.
- falcor84 3y ago
  I'm answering this out of naivete: some people want to benefit humankind over their personal interests.
  - thomastjeffery 3y ago
    In that case, why would you be motivated by a $10m prize?
    - falcor84 3y ago
      To clarify, I as a relatively well-off adult would consider donating towards such a prize pool with the explicit intent of drawing people who aren't as willing or able to give money themselves towards solving a problem that I believe would benefit humankind. That is, I have a personal interest in that outcome (especially as compared to that tech being closed and controlled by governments/corporations) and would be willing to donate money to motivate others to join this effort and make this model open source.
- BeetleB 3y ago
  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?
  - eddtries 3y ago
seafoam 3y ago
Is XTX good for the $10M ? There are a lot of people who got burnt by FTX grants and prizes ...
- eb2 3y ago
  Yes, Alex Gerko is the UKs biggest tax payer and regularly donates to schools/universities math departments
alecco 3y ago
Very cool of XTX. They are a solid company with very smart people. But wouldn't a model capable of doing this be currently worth hundreds of millions? A billion?
- ackbar03 3y ago
  That's why they only offer 10 million. If you want, you can offer 100mio, I'll join your competition instead
daxfohl 3y ago
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.
- ak_111 3y ago
  I totally disagree. I think it is more likely we will have quantum chips running your iphone before this prize gets cashed (and I am a bit of a quantum computing sceptic). For comparison, even field medalists sometime struggle with getting gold medal in the time allocated or identify the trick needed in solving an IMO question. The difficulty difference between solving an IMO level 6 problem and solving an open math problem is much smaller than most imagine.
- killerstorm 3y ago
  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?
  - daxfohl 3y ago
    Yeah I don't disagree with this. But such people do exist. My expectation is that IMO gold is a couple years off. But inventing new math and explaining why it's interesting and useful is much much farther away. I can't decide whether I hope I'm wrong or not.
- esafak 3y ago
  Fancy autocomplete is made possible by understanding. Can you imagine correctly autocompleting a proof to a Millennium Prize problem any other way?
dooglius 3y ago
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.
- quirino 3y ago
  IMO is competitive enough you can't bullshit your way to a gold medal
amai 3y ago
Just combine GPT-4 and Wolfram Alpha?
openquery 3y ago
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] https://arxiv.org/pdf/2305.11014.pdf https://arxiv.org/pdf/2305.11014.pdf
- lacker 3y ago
  No, IMO problems are much too hard for the current generation of theorem provers.
- govg 3y ago
  https://imo-grand-challenge.github.io/ 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.
queuebert 3y ago
Wow, that website has an extremely irritating background animation. Any time your mouse is inside a circle, the circle lights up, stealing your mental focus from the text. Reminds me of the really dumb new Glassdoor design, where it flickers in the background as if it's loading something (but it's not) while you're trying to fill out the sign up form. What is going on with web development these days? Is it some kind of Javascript animation version of the IOCCC?
lupire 3y ago
This is an embarrassing overreach. We don't even have models that can win the far easier AMC, let alone AIME, USAMO, and then IMO.
- mathteddybear 3y ago
  They don't need to win IMO, they need to get a gold medal. I got a gold medal at IMO solving 4 out of 6 problems I don't want to speculate, but it's not inconceivable that this will be achieved by AI within the future lifetime of XTX
- nojvek 3y ago
  What is AMC AIME, USAMO ?
  - supernewton 3y ago
    They're the feeder contests in the U.S. that determine who gets to represent the U.S. in the IMO. AMC = multiple choice test, open to all grade school students. AIME = open response test, all answers are numerical, open to students who score high enough on AMC only. USAMO = USA Math Olympiad. IMO-style proof problems. Open only to top N scorers on AMC and AIME.
- lacker 3y ago
  Well there's a $1m prize for the Riemann hypothesis. Now this is bigger. Which do you think will fall first?
oglop 3y ago
That’s, interesting I think. I’m not sure wha true domain of problems are in that arena. I’ve found great success using LLMs for teaching abstract algebra but have noticed when I switch to analysis or topology things get more wonky. My advice, and I have zero understanding or care why the above happens, is to lean into algebra and train less on analysis. You’ll get there faster it seems.
shannifin 3y ago
Assuming one succeeded, would it be more financially lucrative to claim the prize or form a startup with it?
amai 3y ago
Just combine GPT-4 and Wolfram Alpha? See https://arxiv.org/abs/2308.05713 https://arxiv.org/abs/2308.05713
EVa5I7bHFq9mnYK 3y ago
Such a system would have a market value on $10billions++, nice try trying to get it for 1/1000 the price.
Imnimo 3y ago
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?

281 points by jasondavies 3y ago

> $5mn will be awarded to the first publicly-shared AI model Thank for you the emphasis on openness!

not sure there is much point to this. currently no model is even at the level of primary school math. it will take decades until it can win a gold medal in maths. it won't happen overnight. it will happen slowly. will they still give out the prize in 20 years from now, when it won't seem like such a breakthrough?

up2isomorphism 3y ago

What is fundamentally different about solving IMO compared to solve any other math problems in AI sense?

userforcomment 3y ago

Great marketing stunt, nice work by XTX HR!

gregdoesit 3y ago

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 at the time. It sounded interesting to wonder how far they could go with this kind of approach. I thought they were aiming for the moon: but also respected the boldness and determination. They had the funding to operate for at least a year, and were very focused to get there. Seems like this prize will supr hundreds (or thousands) of teams competing in exactly this space. Perhaps it will have a similar effect like the $1M Netflix Prize in 2009 for recommendations algorithms!

mlengineerio 3y ago
Can you share the name of the startup? I'm also in Palo Alto and tinkering LLM for Match competition too (math.llmlab.io).
anonylizard 3y ago
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.
- dimask 3y ago
  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.
  - anonylizard 3y ago
    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.
    - RandomLensman 3y ago
      AlphaGo solved Go?

arcza 3y ago

Of course XTX is sponsoring this

rvz 3y ago

Great, a worthy competition which being first and correctness completely matter and may the best AI model win. Hopefully DeepMind doesn’t enter otherwise they would smoke everyone else other than OpenAI. Speaking of which, I’ll give you a 1% chance of winning with this paper from OpenAI: [0] with the MATH dataset: [1] EDIT: Why the downvotes? I'm trying to help you here and give you a starting point to win the competition? What's wrong with helping others? [0] https://arxiv.org/abs/2305.20050 https://arxiv.org/abs/2305.20050 [1] https://github.com/hendrycks/math https://github.com/hendrycks/math

daoboy 3y ago

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?

devit 3y ago
It's problem solving (i.e. finding a proof of a statement or finding one or more mathematical objects that have some given properties and proving they have them and possibly that no other objects do), not computation.
- daoboy 3y ago
  That distinction seems really obvious now that you said it. Thank you.
edf13 3y ago
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 < d2 < · · · < dk = n, then di divides di+1 + di+2 for every 1 ⩽ i ⩽ k − 2 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 composite number $ n $ with its divisors $ d_1, d_2, \ldots, d_k $ where $ 1 = d_1 < d_2 < \cdots < d_k = n $, the property $ d_i $ divides $ d_{i+1} + d_{i+2} $ must hold for every $ 1 \leq i \leq k - 2 $. Let's break down the problem: 1. *Composite Number Requirement*: We are looking for composite numbers, which are integers greater than 1 that are not prime. These numbers have more than two distinct positive divisors. 2. *Divisor Property*: The property $ d_i | (d_{i+1} + d_{i+2}) $ means that $ d_{i+1} + d_{i+2} $ is a multiple of $ d_i $. 3. *Systematic Examination*: We will analyze this property systematically for composite numbers starting from the smallest composite number (4) and going upwards. Let's start the analysis: - For $ n = 4 $, the divisors are $ 1, 2, 4 $. Here, $ 1 | (2 + 4) $, so 4 satisfies the condition. - For $ n = 6 $, the divisors are $ 1, 2, 3, 6 $. Here, $ 1 | (2 + 3) $ and $ 2 | (3 + 6) $, so 6 satisfies the condition. - For $ n = 8 $, the divisors are $ 1, 2, 4, 8 $. Here, $ 1 | (2 + 4) $, but $ 2 \nmid (4 + 8) $, so 8 does not satisfy the condition. Let's implement a systematic method to identify such composite numbers up to a reasonable limit (let's say up to 100 for a start) and check if they satisfy the given condition. The composite integers greater than 1 and up to 100 that satisfy the given property are: 4, 8, 9, 16, 25, 27, 32, 49, 64, and 81. Each of these numbers has the characteristic that for all their positive divisors $ d_1, d_2, \ldots, d_k $ (where $ 1 = d_1 < d_2 < \cdots < d_k = n $), the condition $ d_i $ divides $ d_{i+1} + d_{i+2} $ is true for every $ 1 \leq i \leq k - 2 $.

singularity2001 3y ago

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 https://news.ycombinator.com/item?id=38391923 Or at least maybe it will be a good foundation model to be fine-tuned for reasoning?

machiaweliczny 3y ago
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?
- haltist 3y ago
  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.
  - quirino 3y ago
    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.
    - haltist 3y ago
      You gotta be more techno-optimistic. People are just arithmetic and an existence proof that algorithms can be intelligent. People are just math so it's obviously possible to engineer general artififial intelligence with just math and computers. It's all a matter of adding up the right floating point numbers in the right (partial) order (modulo parallelism).
    - 3y ago

7373737373 3y ago

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 bounties. Now, precisely formalizing specific conjectures and ensuring the proof system is expressive enough but doesn't allow for the introduction of any new assumptions is another problem...

xavxav 3y ago
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 online, all that's required is an email.
- 7373737373 3y ago
  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.
  - lupire 3y ago
    Overhead of block chain is greater than overhead of centralization. We already have rich math guys like Simons throwing money at people doing math.
- eddtries 3y ago

andyjohnson0 3y ago

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.

adhocmobility 3y ago
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.
- RugnirViking 3y ago
  general intelligence will become cheap? and so your suggestion is to develop skills outside of skills?
- nickfromseattle 3y ago
  Any suggestions?
  - therealdrag0 3y ago
    Plumber
  - airstrike 3y ago
    AI Software Engineering? Baker?
  - realharo 3y ago
    Stockpile metals and rare earth elements. Natural resources will be the beginning and the end of trade. (not actually serious, at least not yet)
- Davidzheng 3y ago
  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.

svat 3y ago

How does this relate to the "IMO Grand Challenge" https://imo-grand-challenge.github.io/ 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 https://aimoprize.com/supporters)

svat 3y ago
Answering my own question: Alex Gerko (who's behind the $10M prize here) says: > "It came about as me checking on the status of IMO Grand Challenge (which was launched in 2019 https://imo-grand-challenge.github.io https://imo-grand-challenge.github.io) and deciding that it's time to give this idea a boost" https://twitter.com/AlexanderGerko/status/1729207936625627336 https://twitter.com/AlexanderGerko/status/172920793662562733...
dwrensha 3y ago
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 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.
- lupire 3y ago
  "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.
  - dwrensha 3y ago
    > 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.

aaron695 3y ago

[dead]

WhitneyLand 3y ago

Before gold at the math Olympiad, it would be nice if GPT 4 could merely evaluate an expression like this into an exact solution : 3 + 1 / (3 + 1 / (3 + 1/3))

dmd 3y ago
Works for me... https://cloud.typingmind.com/share/29d28743-b6a7-4716-b1aa-a2f03bce16eb https://cloud.typingmind.com/share/29d28743-b6a7-4716-b1aa-a...
- WhitneyLand 3y ago
  That’s helpful thank you. Would you mind trying it 4 times and tell how many succeed? I see it work occasionally but seems <= 50% success rate. See here: https://chat.openai.com/share/6da22a7b-b8f8-4611-b5f7-38048f3414e0 https://chat.openai.com/share/6da22a7b-b8f8-4611-b5f7-38048f...
  - dmd 3y ago
    Worked 6/6 times for me.
    - WhitneyLand 3y ago
      Bizarre, I don’t see how this could be chance. I’m using mostly the ChatGpt client with GPT-4 and no special instructions. Maybe you’re using a model variation via the public API?
      - dmd 3y ago
        I’m using gpt-4-turbo

haltist 3y ago

We will solve math with math and this project will succeed as foretold by prophets of techno-optimism like Marc Andreesen, Elon Musk, and Bill Gates. All we need is the right architecture, aka mathematical formula for giving all of math a smooth manifold structure. How this works for discrete structures like integers is left as an exercise for the reader and future AI which will figure out how to improve themselves and deal with discrete and non-smooth mathematical problems. I can win this challenge by the way for $80B. I already know what architecture is required to solve math with math but I need the money to buy the GPUs. You might think such a recursive application of math is logically circular but it is not and all I need is $80B to prove it (pun intended). Claude did not like this comment at all, ironically: I do not have enough context to fully evaluate those claims or determine if that approach would work. Solving all of mathematics is an extraordinarily ambitious goal that would require fundamental theoretical advances we do not yet possess. While future AI systems may someday make significant progress on longstanding mathematical problems, making definitive claims about solutions requires rigorous mathematical proof and analysis beyond optimistic speculation. I'd encourage focusing discussion on specific mathematical questions or areas of research rather than making broad, unsupported assertions about solving all of mathematics.

WhitneyLand 3y ago

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.

haltist 3y ago
I sense you are a techno-optimist.
- WhitneyLand 3y ago
  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
  - haltist 3y ago
    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.
    - ShamelessC 3y ago
      Are you serious? edit: you’re either trolling or mentally ill. If it’s the latter, I sincerely apologize. Hope things get better for you soon. edit edit: I saw your comments about the art project. Thank God. I didn’t want to live in a world where someone like that existed.
      - deleted 3y ago
        [deleted]

Yhippa 3y ago

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?

nathanfig 3y ago
Some private enterprises would undoubtedly ignore this prize, but a lot of academic researchers (including students) would be more than motivated by this prize.
falcor84 3y ago
I'm answering this out of naivete: some people want to benefit humankind over their personal interests.
- thomastjeffery 3y ago
  In that case, why would you be motivated by a $10m prize?
  - falcor84 3y ago
    To clarify, I as a relatively well-off adult would consider donating towards such a prize pool with the explicit intent of drawing people who aren't as willing or able to give money themselves towards solving a problem that I believe would benefit humankind. That is, I have a personal interest in that outcome (especially as compared to that tech being closed and controlled by governments/corporations) and would be willing to donate money to motivate others to join this effort and make this model open source.
BeetleB 3y ago
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?
- eddtries 3y ago

seafoam 3y ago

Is XTX good for the $10M ? There are a lot of people who got burnt by FTX grants and prizes ...

eb2 3y ago
Yes, Alex Gerko is the UKs biggest tax payer and regularly donates to schools/universities math departments

alecco 3y ago

Very cool of XTX. They are a solid company with very smart people. But wouldn't a model capable of doing this be currently worth hundreds of millions? A billion?

ackbar03 3y ago
That's why they only offer 10 million. If you want, you can offer 100mio, I'll join your competition instead

daxfohl 3y ago

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.

ak_111 3y ago
I totally disagree. I think it is more likely we will have quantum chips running your iphone before this prize gets cashed (and I am a bit of a quantum computing sceptic). For comparison, even field medalists sometime struggle with getting gold medal in the time allocated or identify the trick needed in solving an IMO question. The difficulty difference between solving an IMO level 6 problem and solving an open math problem is much smaller than most imagine.
killerstorm 3y ago
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?
- daxfohl 3y ago
  Yeah I don't disagree with this. But such people do exist. My expectation is that IMO gold is a couple years off. But inventing new math and explaining why it's interesting and useful is much much farther away. I can't decide whether I hope I'm wrong or not.
esafak 3y ago
Fancy autocomplete is made possible by understanding. Can you imagine correctly autocompleting a proof to a Millennium Prize problem any other way?

dooglius 3y ago

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.

quirino 3y ago
IMO is competitive enough you can't bullshit your way to a gold medal

amai 3y ago

Just combine GPT-4 and Wolfram Alpha?

openquery 3y ago

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] https://arxiv.org/pdf/2305.11014.pdf https://arxiv.org/pdf/2305.11014.pdf

lacker 3y ago
No, IMO problems are much too hard for the current generation of theorem provers.
govg 3y ago
https://imo-grand-challenge.github.io/ 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.

queuebert 3y ago

Wow, that website has an extremely irritating background animation. Any time your mouse is inside a circle, the circle lights up, stealing your mental focus from the text. Reminds me of the really dumb new Glassdoor design, where it flickers in the background as if it's loading something (but it's not) while you're trying to fill out the sign up form. What is going on with web development these days? Is it some kind of Javascript animation version of the IOCCC?

lupire 3y ago

This is an embarrassing overreach. We don't even have models that can win the far easier AMC, let alone AIME, USAMO, and then IMO.

mathteddybear 3y ago
They don't need to win IMO, they need to get a gold medal. I got a gold medal at IMO solving 4 out of 6 problems I don't want to speculate, but it's not inconceivable that this will be achieved by AI within the future lifetime of XTX
nojvek 3y ago
What is AMC AIME, USAMO ?
- supernewton 3y ago
  They're the feeder contests in the U.S. that determine who gets to represent the U.S. in the IMO. AMC = multiple choice test, open to all grade school students. AIME = open response test, all answers are numerical, open to students who score high enough on AMC only. USAMO = USA Math Olympiad. IMO-style proof problems. Open only to top N scorers on AMC and AIME.
lacker 3y ago
Well there's a $1m prize for the Riemann hypothesis. Now this is bigger. Which do you think will fall first?

oglop 3y ago

That’s, interesting I think. I’m not sure wha true domain of problems are in that arena. I’ve found great success using LLMs for teaching abstract algebra but have noticed when I switch to analysis or topology things get more wonky. My advice, and I have zero understanding or care why the above happens, is to lean into algebra and train less on analysis. You’ll get there faster it seems.

shannifin 3y ago

Assuming one succeeded, would it be more financially lucrative to claim the prize or form a startup with it?

amai 3y ago

Just combine GPT-4 and Wolfram Alpha? See https://arxiv.org/abs/2308.05713 https://arxiv.org/abs/2308.05713

EVa5I7bHFq9mnYK 3y ago

Such a system would have a market value on $10billions++, nice try trying to get it for 1/1000 the price.

Imnimo 3y ago

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?