$10M AI Mathematical Olympiad Prize
aimoprize.com
aimoprize.com
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!
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.
An analogy: If it takes 20 years to create AGI equivalent to the village idiot. It take another couple of hours to go from that to Einstein.
Imo we are not currently in the beginning of an exponential curve re solving math with AI, and def not on the path of AGI. I understand that if one believes that we are on the path to AGI soon then we shall have these math-AI advancements quite soon, but I disagree with the premise.
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.
Not sure. Art is about approximate pattern recognition and if you have a large enough dataset it seems that you can definitely reproduce some of that.
For math... it involves consistent reasoning from A to Z - which does not allow for any kind of mistake in the way. In Art you won't feel too bad if the shadows or the lights are a little weird or if a character has 7 fingers instead of 5 on one hand, but this kind of mishaps break everything in Math.
I think artists would disagree with your assessment of 'approximate pattern recognition'. Its more like：
1. Given a set of words describing what the user wants. 2. Arrange pixels in a grid 3. That maximizes the user rating
On one hand it is tolerant of small errors. On the other hand its an extremely broad problem. Also to get a good user rating, it has to do 99 things right for every 1 thing it draws wrong.
Now, if we end up seeing mastery, that would be extremely interesting.
No no, you see I prompted the AI with "masterpiece, photorealistic, 35 mm photography, cinematic, dslr, volumetric lighting, trending on artstation, 4k, 8k, hyper-detailed, epic digital painting by Greg Rutkowski" /s
Someone can tell you when a math problem is solved. Someone else can't tell you when you've successfully art'd with remotely the same degree of confidence. In so far as they can, however, many experts claim that AI cannot, indeed "do an art".
Also, it's easier to formulate a hard math question (there are plenty of unsolved problems), but that's (IMHO) harder to do for art. Sure, you may think this is the first time the phrase "Astronaut riding a Llama and holding an avocado" was writ, but those are all well represented concepts in the dataset. For more abstract prompts, there really isn't a way to verify "correctness".
If I was asked to draw
a. the emptiness in your heart
b. the lack of furniture in your room
c. your empty bank balance
d. starvation
e. object returned by a python function with no return
...
I could just submit an empty sheet of paper, & an artist would argue that my empty sheet of paper represents any/all of the above.
Now, if I turn in the same empty paper at a math qualifier and argue that it represents the infinite set of real and complex numbers, ergo the answer to the posed qual problem must be in there, I'll get kicked out of that phd program in a jiffy.
And they'd be taken about as seriously as the ads taped to a urinal in a Museum of Modern Art washroom.
In a way it is, in a way it isn't. You have to remember what is easy for machine isn't going to correlate to what is easy for us humans. Look at AI art. Closely. No, closer than that. All the detail is fucked up. Not just the hands, but the tiniest of things. Strokes, lighting, reflections, and consistency, and all that. But can I turn my friend into a convincing werewolf? Yes. Can I turn my cat into a human or Wonder Woman? No. The system isn't a "fancy copier" but it is a compression algorithm and the aforementioned tasks were only possible because lots of work training LoRAs, textual inversions, control nets, and so on (you could seriously improve GANs, VAEs, hell, even Boltzman Machines could probably do pretty well were any of these given the same research investment that diffusion has received. GANs come close but nuances like GANs having a magnitude fewer parameters).
But let's look at math, can I consistently add numbers? No. The problem is that in math, all those tiny intricate details matter. Not only that, they matter at every single step. The thing here is that these are still pattern recognition machines. But they aren't generalized machines. You can't really derive out all of math from probability distributions (or at least cleanly, but still not convinced you can). The thing is that for math to work in AI we have to address the elephants in the room: math. Yeah, math. ML people don't like it. But we gotta address the axioms in the room that we're operating under. How do we move on from machines operating on manifolds? How do we make it so data are not distributional? How do we move away from a number of unmentioned axioms remains a large open problem in AI research. One that does not get anywhere serious enough of a conversation, especially within the community. Sure, maybe transformer circuits can learn some addition by learning how to do FFTs and add in the FFT space, but you're not going to get to Abstract Algebra that way. Ideally the AI can solve problems that have no algorithms, pun intended.
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.
Solving Go means determining by what margin the first player can win, or equivalently, at what komi for white the game is a theoretical draw.
That also makes it dependent on the exact rule set used.
E.g. 2x2 go is a +1 first player win with the Tromp-Taylor rules of Go, while the Japanese rules are not even sufficiently formalized to allow scoring a 2x2 game.
Suppose that P1 passes on their first move (which is a valid move). Then P2 has a winning path of play in which they put down the first stone. But P1 could have made that move and then they would be on the winning path.
First player does not always have the advantage. Nim is the best example where the setup can either be the first player winning game (nim-sum of the sizes of the heaps is not zero) or the second. My understanding is also that Chess (another perfect information turn-based game) is not shown solved or even has proven first player advantage (though in practice it looks so).
So I get the argument, I just don't buy it. I would be inclined to lean towards that direction, but it's a tough claim theoretically and probably not meaningful in practice (unless a generalized strategy such as strategy stealing can be employed otherwise a lookup table is impractical as it'd contain more bits than atoms in the universe even for 100 move games).
I think we have to consider far more than strategy-stealing which is not even a generalizable strategy to two-person perfect information turn-based games.
https://en.wikipedia.org/wiki/Nim#Proof_of_the_winning_formu...
First, I thought going first in chess is generally considered an advantage. Even the wiki article states that. Or at least says there's a 10% increased win rate.
Second, I still don't get why passing is the important aspect. I thought the important aspect is symmetry. I mean I can understand this in nim since that symmetry is that killer aspect that makes for the easy analysis of a solution.
When I said I'm not a game theory person I didn't mean I have no game theory experience but that's not what I study. I'm on the mathy side of ML but not so much in RL. You can use math with me if that makes things easier (in fact, I love math. Please do. RL notation doesn't scare me but rather weirds me out that it scares others) because I think we're getting lost in the conditions.
I'm not a mathematician myself, just got into this stuff when I was working on a boardgame solver. I find it difficult to map the 'symmetric game' definition "the payoffs for playing a particular strategy depend only on the other strategies employed, not on who is playing them" onto a turn based game, but if it can work for Hex it must be compatible.
If you consider a strategy to be "a decision tree for how to place stones, when I'm playing as 2nd", then there's perfect symmetry between being 1st and choosing to immediately pass, and being 2nd. The possible strategies and resulting payoffs are the same. You add on top the extra move, which the possibility of passing means is at worst neutral for 1st player, and they cannot be at a disadvantage.
More intuitively for me: being allowed to pass your first move is the same as getting to pick which side you want to play. There's no way the side who can pick to play 1st or 2nd at their option can be at a forced loss to the side who just has to accept their decision. The picker would just pick the other side and now they have a forced win.
(I'm always assuming above any kind of infinite-pass-standoff is a draw, and not some kind of weird other thing).
If I haven't expressed my thoughts clearly enough that's probably about as well as I can manage I'm afraid.
Yeah so probably the better way to think about it might be with the payoff matrix. Because symmetry is actually about the strategy. That's why there are the notes about the laddering in Go. But the payoff of a symmetric game is actually when A = -A^T. So if we have a 2x2 game a symmetric zero-sum one is where the payoff matrix might look like [[0, 1], [-1, 0]] Where we're like an inverse-identity matrix (actually anti-symmetric) but the diagonals are opposite. Maybe it is best to think about this from a geometric perspective, this symmetry here (in this specific example) is a rotation matrix. That's what it does when applied to another matrix. Recall our standard form is [[cos(theta), -sin(theta)],[sin(theta), cos(theta)]]. Pretty easy to get our matrix from there if you remember that cos(90)=cos(180)=0 and sin(90)=1 but sin(180)=-1. So our angle of rotation is 180 degrees (or pi radians). You could also see that if we made the two columns vectors we'd see they pointed in opposite directions. That's the symmetry! Okay, yeah, maybe that's confusing lol. But I find it helpful to see matrices as transforms and I wish this was stated a bit more clearly and often.
So now that we maybe understand that, symmetry is about a __strategy__, not a player. Because our payoff matrix is strategy based. For example, our strategy for rock-paper-scissors is to pick each outcome 1/3 of the time, which gives us this symmetric payoff. But if we pick rock every time we don't get that payoff, right? So it's actually not about who goes first or second but also includes the strategy aspect.
At least that's my understanding which a lot is prompted by this conversation (thanks!)
The reason I'm finding the go argument hard is thinking of a basic "entropy" based strategy (it'll serve you well in boardgames, especially when sight reading). The idea is if you don't know the best move, play the move that gives you the most future moves. It'll trick you into thinking that this strategy is actually simple, it isn't. So in the game of Go, this isn't reasonably different from making a random move! Because there are just so many. And realistically your strategy is going to be the composition of many different strategies. Like you said, pull out the decision tree but we can actually abstract this a bit more and have a decision strategy tree that's a superset to our strategy that's a response (e.g. a ladder is set up so we play the laddering strategy). The reason I'm not buying the argument isn't about the logic, it is about the possible move sets. Even with super-ko (the board cannot return to a state it has previously been at any time in the game (must be fun to keep track of...)). So forgetting about all the extras that are played in go, passing shouldn't result in a meaningful change in the number of possible strategies. But this argument might actually be an argument in favor of symmetry, not against it. Coming back to Chess, we know that game __is not__ symmetric. Why? Because white has different strategies than black. If instead the first "move" is to flip a coin and that decides who is white and who is black, then the game actually becomes symmetric. Kinda wild...
I didn't read this, but a glance suggests that black dominates in smaller games
http://erikvanderwerf.tengen.nl/pubdown/thesis_erikvanderwer...
Does second mover in Go have some sort of artificial benefit in scoring or playing? As in -- is there something to compensate for moving second?
On the face it seems like first mover would have an advantage in any turn-based game. But maybe, in some games, seeing an opponent's strategy is more helpful than executing the strategy.
Also, are there examples of real games where second mover can always win? (Real as in, not made up with weird rules just to demonstrate it's possible.)
Yes. The second player typically gets an extra 6.5 or 7.5 points.
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 millennium problem, but it is very interesting and suggests fairly sophisticated conceptual understanding of mathematics nevertheless.
Current architecture and training methods I don't think are enough to get there. However, with enough compute, I can plausibly envision some sort of meta training of LLMs using an analogy to GANs where one network tries to synthesize new correct ideas and the other shoots them down as not novel, not correct, or not sufficiently interesting.
Such an approach I think could perhaps work, but the compute needed would probably be pretty high.
They decompose problems, solve specialized subsets, examine more general cases, use existing proofs, do some numerical analysis, etc.
Solving Millennium problems is a whole different ballgame. It's not known if these problems are solvable within ZFC axioms. (In one case, the Yang-Mills prize, stating the problem mathematically is part of the challenge.) All of the obvious applications of known tricks have been tried and failed. To solve such problems, one probably has to invent new and surprising mathematical definitions, building a framework in which the problem becomes solvable. This is something that LLMs will be crap at; the process of invention is not represented in any training data we have access to.
There are ~1000 MO winners and 1 (one) Millenial problem solver ...
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."
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.
1. https://economicsfromthetopdown.com/2022/04/08/the-dunning-k...
But Gwern has written about some earlier debunkings of the D-K effect, ad furthermore D-K was never about the popular misconception of D-K ("incompetent people think they are more competent than competent people").
https://en.wikipedia.org/wiki/Overconfidence_effect
Or even
I'm building something myself that I hope will be able to work similarly: https://aiconstrux.com
Or will he be doing it after the fact, when the questions are published.
Today we see multiple billion dollar recommender systems, like Tiktok. Netflix ironically benefits the least from recommenders due to the nature of its dataset (Very expensive, low sample size).
Today Netflix is in the "how do we get our customers to use our service as little as possible but still pay us every month" phase of their mediacom hypocracy. From a business standpoint, that is their best optimization. They are AOL/TW from 20 years ago.
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.
"Informal to informal" is so far snake oil.
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.
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).
> "It came about as me checking on the status of IMO Grand Challenge (which was launched in 2019 https://imo-grand-challenge.github.io) and deciding that it's time to give this idea a boost"
https://twitter.com/AlexanderGerko/status/172920793662562733...
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...
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.
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.
We already have rich math guys like Simons throwing money at people doing math.
Ultimately, I don't think this is really practical, and investing in AI proof agents is the way to go.
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.
No idea about the minting process, there seems to be an infinitude of possibilities.
Blockchains are append-only databases, sometimes (usually?) with 'slow' thrown in somewhere.
That’s an app on top of the append only DB with some logic that either requires IRL groups to manage it, or a blockchain contract. I prefer the latter tbh!
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.
[1] pseudonymous (in case of BTC) if we're being pedantic.
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?
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.
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.
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 talks about rate of profit over the economy as a whole. It says nothing about the distribution of said profits. Its assumed that human labors are the ones also reaping some of those profits because they are doing labor, hence wages from those labors remain stable. If for some reason there was 0 labor available to you the same premise could hold true, the rate the AI is earning could remain stable, you're just shit out of luck.
I'm not quite sure what you mean. Isn't math already pretty much the most accessible thing that could be imagined? I can't think of any story of someone in the past century who wanted to study math but was unable to, except for reasons prohibiting any sort of academic study whatsoever (e.g. girls in Taliban controlled areas).
Or is it about making this more accessible to students who are "merely good" rather than brilliant?
Except it'll be available 24/7 and you won't have to pass exams, spend $$$$, attend full time, and live in dorms and be in your late teens or early 20s to get access.
That analogy occurred to me too. But I'm not sure what the corresponding higher-level domain is that mathematicians might have to migrate to - in the way that assembly programmers started using high level languages. Writing prompts for maths LLMs, or wrangling teams of them, is hardly going to be well paid enough to facilitate a decent life in this era of late capitalism, or even pay uni fees.
And even if there are such higher-level domains, its not certain that they are compatable with available human cognitive ability or limits.
Lots of maths grads currently go into tech/finance/lifescience/whatever. I'm a dev and I can see those fields being eaten alive by this stuff. I don't want my kid to end up as a 2030-equivalent of a fully qualified assembly language programmer.
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?
I wouldn't worry too much.
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.
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 mathematician in this case is far less skilled than the bot, but that doesn't detract from their market value. Most programmers are way less skilled/smart than the library authors that they rely on, that doesn't stop them from earning $$$, because they are useful.
https://www.reddit.com/r/math/comments/l7yyir/not_joking_uni...
https://www.reddit.com/r/math/comments/15of64l/rumor_west_vi...
Joking aside, of course it is not on you to provide evidence. I would probably start with seeing how many universities have pure math departments over a time axis from now back to 2000 or so.
It might even be that the total funding increases, but is more centralised in the big universities. So a total funding timeline would also be good.
Or perhaps not. In that blog, Gelman speaks of Gregg, who ended up as a GS VP, and says -
math olympiad = high school basketball star
pro mathematician = NBA player
Goldman Sachs VP = sports hustler
I actually worked with Gregg in fixed income at that time :) Gelman's blogpost received sufficient notoriety, atleast within GS & the IB community.
(not actually serious, at least not yet)
It will still require sound mathematical knowledge and understanding, to know what are the interesting questions to ask. Even if AI knows all the answers, it doesn't change anything because the answers already exist anyway.
Math shapes your mind, that’s why we learn it.
But wouldn't a model capable of doing this be currently worth hundreds of millions? A billion?
If you want, you can offer 100mio, I'll join your competition instead
Thank for you the emphasis on openness!
(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.
How well do current gold medalists do in trading?
Higher level math is nothing like the math used in trading algorithms. It wouldn't be any more useful than a top tier PHD graduate.
There are a lot of people who got burnt by FTX grants and prizes ...
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.
Do you consider AI to have already considered substantially to the advancement of science?
For example AlphaFold, Weather forecasting, Algorithm optimization, etc
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.
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.
How many people you know who came up with an interesting new branch of math?
I can't decide whether I hope I'm wrong or not.
Can you imagine correctly autocompleting a proof to a Millennium Prize problem any other way?
3 + 1 / (3 + 1 / (3 + 1/3))
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-38048f...
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?
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.
Or at least maybe it will be a good foundation model to be fine-tuned for reasoning?
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?
Is there a clear point of departure when AI can no longer handle mathematical reasoning?
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 \).
I tried an easier problem, extending Rolle's theorem to the multidimensional case with Poe.com:
Prompt: Let U be an open subset of R^n with compact closure K. Suppose f: K → R is continuous on K, differentiable on U, and satisfies f(x) = 0, for all x in K \ U. Show that there exists a in U with grad f (a) = 0.
Poe: To prove that there exists a point a in U such that grad f(a) = 0, we will utilize the concept of connectedness and the Mean Value Theorem.
Since U is an open subset of R^n with compact closure K, we know that K is a closed and bounded subset of R^n. Furthermore, since K is a compact set, it is also a connected set.
Now, let's define a new function g: K → R^n such that g(x) = (f(x), f(x), ..., f(x)) for all x in K. In other words, each component of g is equal to f(x) for all x in K.
Since f is continuous on K and differentiable on U (which is an open subset containing K), it follows that g is continuous on K and differentiable on U.
Consider the function h: K → R defined as h(x) = ||g(x)||^2 = f(x)^2 + f(x)^2 + ... + f(x)^2 = nf(x)^2.
Note that h is continuous on K since g is continuous on K and ||.||^2 is a continuous function.
Now, let's consider the set S = {x in K : f(x) = 0}. Since f(x) = 0 for all x in K \ U, we have K \ U ⊆ S. Therefore, the set S is closed.
...
Stochastic parrot indeed.
Higher level math becomes pretty verbose so enters the domain of language more so than pure symbolic computation. However there is still complex reasoning under the hood. Gpt-4 in ChatGPT flounders when I ask it questions from my thesis, so I’m not sure how it will do with problems it hasn’t seen, where it needs to apply “new” reasoning.
I’d love to know if in your example, GPT is reciting something it’s seem verbatim, or if it is taking multiple sources and combing them.
That's hilarious
"The condition fails for i=1 since 1 does not divide p+q unless p+q is a multiple of n, which is not generally true" (1 divides everything)
In the second it gives up:
"However, this conclusion is based on heuristic reasoning and examples"
Third attempt it makes this mistake:
"If the immediate next divisor, di+1 , is not a multiple of p (for instance, it could be q or a product involving q), then p does not divide di+1. Hence, p will not divide the sum di+1+di+2 in such a case, violating the condition." (the fact that p does not divide d_i+1 does not imply that it does not divide d_i+1, d_i+2)
Then it gives up again: "However, this conclusion is based on heuristic reasoning and examples"
Then it makes this basic logic mistake: "However, since p and q are distinct primes, p does not divide q, and it's not guaranteed that p divides q+d_i+2 , especially if d_i+2 is not a multiple of p. Therefore, for such n, the condition fails." (the fact that "it's not guaranteed" doesn't imply that it's false)
Overall it proves that prime powers have the property, conjures that non-prime-powers don't, proves that p*q doesn't have it, but completely fails at coming up with a proof strategy that proves that non-prime-powers don't have the property.
Amusingly, the list of the integers <= 100 satisfying the property is correct, and it contradicts itself from the previous paragraph. Maybe if GPT wasn't a one-directional autoregressive model but allowed itself to go back and edit the past, it would have caught up that discrepancy and fixed it - but no such architecture currently exists that would run in decent amount of time.
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...
Unless I'm getting myself completely wrong, this also seems to be a very unusually simple problem for IMO's standards. I don't think I ever got myself solving one of them when I tried in the past, but if I'm not fooling myself the most natural approach for this one seems to bring to the solution:
1) Look at the two smallest divisors 1 < d_2 < d_3 of n. Then d_2 is necessarily a prime p, and d_3 is either p^2 or a different prime q. Let's first prove the latter can't be the case: if it where, looking at the biggest 3 divisors [n/q, n/p, n], we'd get that there's an integer a such that: n/q * a = n/p + n. Simplifying a bit, we get (1+p)q = ap, which is impossible because p divides neither p+1 nor q.
2) So, for n not to be a power of p, it must be 1 < d_2=p < d_3=p^2 < ... d_{k+1}=p^k < q. In particular, p^{k-1} must divide p^k+q. However this is also impossible, because p^{k-1} obviously divides p^k, but not q, so it can't divide the sum.
Gosh I feel like a grumpy old man saying "those youngsters, on my days we used to have harder problems than this" ;-)
1)notice it's prime powers
2)notice that 1,p,p^2 eventually leads to contradiction
3)use the last part of the factorization to rule out 1,p,q
I couldn't get GPT4 to do either 2 or 3 even with hints. It's surprising that either due to context length or something else I feel like its reasoning abilities are worse when you try to guide it. But maybe this is true for humans too.
Nevertheless, I think the more important question is whether GPT-4 is capable of
1) Listing all solutions less than 100
2) Figuring out the commonalities of the solutions
For 1) I have no doubt that the answer is yes based on its coding skills, in fact it is much stronger at coding than this. For 2) my subjective feeling in playing around with it is it's not consistent at similar problems but it can do it sometimes. Maybe in this case it has seen the list of prime powers <100 so it's very easy for it.
﷽!
Rewrite this post using unicode characters:
> The IMO are a bit more involved...
Answer:
> 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 d₁, d₂, ..., dₖ are all the positive divisors of n with 1 = d₁ < d₂ < ... < dₖ = n, then dᵢ divides dᵢ₊₁ + dᵢ₊₂ for every 1 ≤ i ≤ k − 2
Although ChatGPT 4 makes a pretty decent start on this already:
> To determine all composite integers 𝑛 > 1 that satisfy the given property, we need to closely examine the condition set forth: for a composite number 𝑛 with its divisors d₁, d₂, ..., dₖ where 1 = d₁ < d₂ < ... < dₖ = 𝑛, the property dᵢ divides dᵢ₊₁ + dᵢ₊₂ must hold for every 1 ≤ i ≤ 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ᵢ | (dᵢ₊₁ + dᵢ₊₂) means that dᵢ₊₁ + dᵢ₊₂ is a multiple of dᵢ.
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 𝑛 = 4, the divisors are 1, 2, 4. Here, 1 | (2 + 4), so 4 satisfies the condition.
- For 𝑛 = 6, the divisors are 1, 2, 3, 6. Here, 1 | (2 + 3) and 2 | (3 + 6), so 6 satisfies the condition.
- For 𝑛 = 8, the divisors are 1, 2, 4, 8. Here, 1 | (2 + 4), but 2 ∤ (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₁, d₂, ..., dₖ (where 1 = d₁ < d₂ < ... < dₖ = 𝑛), the condition dᵢ divides dᵢ₊₁ + dᵢ₊₂ is true for every 1 ≤ i ≤ k − 2.
I'm more interested in the point where AIs are presenting proofs far beyond human capability. I'm imagining a day when an AI says it has solved some interesting problem and when we ask for the proof it spits out a 4 million page document. What are we supposed to do with that? What's the role of humans in that world?
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?
We don't even have models that can win the far easier AMC, let alone AIME, USAMO, and then IMO.
I don't want to speculate, but it's not inconceivable that this will be achieved by AI within the future lifetime of XTX
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.
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.