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!
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.
Their current ambition is to be able to solve school math, which is quite far away from solving unsolved conjectures or math olympiads. I really doubt that any of this is within LLM/transformer scope, except maybe in some auxiliary sense to other, much different architectures.
Art isn't an easier problem than math. An artbot would have sounded more sci-fi than a mathbot only 2 years ago.
Yet it only took the AI world 1.5 years to go from drawing child scribbles to replicating top artists with like 90% similarity (I can barely tell the difference between AI and human drawn art anymore with the new NovelAI model). It won't be long before AI starts to go superhuman in art skills.
It won't 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.
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.
To nitpick a little further, it actually is not possible that the second player has a winning strategy. For that to be the case, P2 would need a winning path of play no matter what P1's first move is.
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.
I'm not a game theorist, in RL, nor a big Go player; but I am having a hard time finding this argument convincing. Isn't the whole reason Go is impressive is because the enormous set of possible moves? Like we know that no computer could run ever game in the lifetime of the universe were it to even perform millions of moves a second. So of the I understand this number to be north of 10^500 for possible legal and playable games. So the difference of 1 doesn't seem meaningful. Is there something I'm missing or a more convincing argument? Because even if player 1 always locks out 90% of those possible future moves, that's still an absurdly large search space and it doesn't seem like it is meaningfully different.
It's a proof by contradiction, like the halting problem proof. It doesn't rely on the actual playable games at all, but what the existence of a winning strategy would imply. If there was a guaranteed winning strategy for player 2 it would be contradictory because player 1 could execute it by passing their first turn then using the winning P2 strategy. In that game both players can't be guaranteed to win, so there must be some flaw in P2's supposed guaranteed win strategy. https://en.m.wikipedia.org/wiki/Strategy-stealing_argument
I am familiar with strategy stealing and things like tit-for-tat. But even the wiki article you linked suggests that Go is not a symmetric game, which is the requisite condition for strategy stealing to work (which was my underlying belief albeit (very) poorly worded). The wiki suggests both ladder and ko fights create an asymmetry as well as central control. Not to mention Komi explicitly making it asymmetric.
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.
The passing is the important part. In chess you can't pass so going first might be bad, you could be the first to reach a forced zugzwang. If you have the option of passing your first turn, then having a turn before the 2nd player gets to go is at worst neutral for you. Likewise in Nim you can't pass and taking your turn might be bad for you unlike Hex.
Sorry, I'm not quite following, there seems to be a disconnection.
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.
Oh yeah, in chess going 1st is 100% definitely an advantage. For example, pawn to a4 is a really bad opener because its so close to throwing away that advantage by passing your first turn. Its just that the rules permit that taking a turn can force you into a worse position than you started, and you can't prove the starting position isn't like that. So from a proof perspective the empirical truth that going first is really good is not particularly helpful. The passing thing is weird because it empirically is a bad idea, it just closes a theoretical loophole.
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.
> 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,
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
I would assume this is possible for any sufficiently complex game. Would you mind answering a few questions from someone near-completely ignorant about Go?
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.)
> solve go (Ie, can the first mover guarantee a win?).
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.
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.
Fingers are already mostly solved. The latest models draw hands better than most human artists.
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.
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 commonality. Thing is the wide audience chews in mediocrity all the time, and nobody seems to have been able to change this for ages...
> Mediocrity is exactly what we'd expect from such an approach.
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
I think art is much easier for LLM-style AI models to do compared to writing.
To make a nice picture you just need to place pixels near each other in a way that looks good, and we all know LLMs are phenomenal at this.
Good text on the other hand is not just text that has a good flow and fits the prompt. It must follow a line of thought, and LLMs don’t do that by design, even though we could argue wether they have that capability as an emergent one, but I don't believe that at all.
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".
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.
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.
I don't disagree, as in that if we achieve school math in a way that is not mere overfitting over a language-based training set, going to more advanced mathematics is definitely conceivable. My problem is that people are talking about solving unsolved conjectures while we are not even in a point where we know how to tackle math at all.
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.
That's 4-5 years for solving Olympiad problems. Those are just very tricky high school math problems. They have solutions and can generally be solved by applying some combination of standard tricks. It's very much the sort of thing an LLM should be good at.
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.
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.
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."
I have a couple friends who did the Math tripos at Cambridge (so a pretty high level!) who work in tech and have unanimously said they have 0% expectations of an LLM doing a millennium problem anytime soon
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 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.
And also if you could combine that with some kind of representation software like Lean that can validate proofs, perhaps you can generate some kind of targeted search of the problem space and with a combination of a general high level strategy and maybe brute force of some sub-problems, find novel solutions. My understanding is that is the common human approach: gain some kind of intuition of problem, try a few things and then iteratively refine. Sometimes that works, sometimes you need to find a new starting point. It seems plausible we could automate that workflow, with likely mixed but still useful results.
I’m not trying to understate the stuff you can do with LLMs or formal proof tooling that could be attached to randomly try things till it reaches a solution to a novel problem, but some solutions you see to lesser problems are sometimes so pie-in-the-sky I think stumbling on one is barely better than a random walk. And I think mathematicians like Tao are far better at narrowing that down. As an aide I can see it’s use, I just don’t believe we’re going to have LLMs & tooling solve these grand problems until compute power is orders of magnitudes better, and even then I’m still sceptical. BUT I’m not a mathematician and this is based on my intuition from pub talks :)
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.
The field of LLM reasoning is far from stable atm. I think it's pretty hard for anyone to give confident predictions about what they can or cannot do in 5 years. In that light, I am skeptical about any claims that they cannot do something anytime soon.
What does an LLM really do? And can it create sometimes entirely novel math that goes against its training set to solve something, and know it’s right using a proof tool that may not even accept that? I agree but on a different order of magnitude of years.
I don't think the actual winning algorithm itself was used, because real world systems have more constraints/requirements than what the recommender was trained on. But that was in 2009, pre deep-learning/AI summer, and $1 mil clearly helped stimulate interest in that area.
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).
My understanding was that their research on what drove engagement shifted quite a bit. Things like social proof, and product patterns like auto-loading the next episode to binge drove engagement metrics. Recently there were some articles about their team custom-identifying which cuts of a video to show as a trailer maximized engagement on a personal level. In some sense that is a recommendation, but it is a broader problem space.
I have a more cynical take; the recommendations declined when Netflix started producing their own content. Prior to this, what constituted a "good recommendation" was aligned between Netflix and the customer, but afterwards not so much.
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.
your sense of humor is much appreciated. couldn't have said it better. hah :) basically i would suggest the study to expand to everyone doing anything titled AI at this moment.
While I get your point and agree, there apparently is no Dunning-Kruger effect. It was determined to be yet another case of faulty data analysis in behavioral psych.[1]
That paper was thoroughly rebutted when posted to HN.
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").
That first article cites more behavioral psych research, which has the absolute worst track record of data analysis. After so many retractions and scandals, I find it difficult to know what to believe anymore.
I'm sure lots of people have been thinking/working along that direction. I think the idea of combining LLMs with formal verification/proof assistant tools (Lean, Coq, Isabelle,...) is particularly interesting. Anyone is aware of any major groups working on open source solutions for this?
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?
> 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 \).
You can just ask GPT-4 to rewrite it using unicode characters:
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.
That's 300 words for saying "in order for n to satisfy the requirements, it must satisfy the requirements."
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.
Yeah, this is actually a really good example of its weaknesses.. it's the equivalent of a bullshit essay in math form. Completely tautological, with just a bit of the correct definitions thrown it to seem like it understands.
That is impressive! It does look like a textbook question so I wouldn’t be surprised if a formulation almost identical to this is in the training data. But the ability to parse the “mathiness” is still impressive.
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.
> 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.
A decent start? It says absolutely nothing about how to solve it, except repeating the question. The part where it tries out the few first numbers is entirely wrong, given that 6 does _not_ satisfy the condition (2 does not divide 3+6=9) and 8 _does_ (2 does divide 4+8=12).
Amusingly, the list of the integers <= 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...
Good to know it can do that, in the pasted chat above it didn't. To be honest, it surprised me it couldn't, this isn't exactly a very hard guess given the computation results. It doesn't convince me GPT4 is anywhere close to winning the IMO, though :-)
True. I let it continue and even prompted it with hints but it cannot find the proof that non-prime powers fail. It can however prove prime powers work.
It's a good point. The knowledge cut-off says Jan 2022, but in the past there's been reasons to suspect some data after the cut-off is in the model too. There's also the possibility that it has seen the problem somewhere else before Jan 2022.
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.
(I'm also replying myself concerning the problem itself).
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" ;-)
haha yeah seems like there's like only three things to do.
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.
GPT-4+code is surprisingly good.
https://chat.openai.com/share/ad42d09a-b366-4b21-b701-782fc8...
"This observation leads to a hypothesis: only the powers of prime numbers satisfy the given condition. To verify this hypothesis, we need to consider why powers of primes might uniquely satisfy the divisibility condition and then prove or disprove it."
In my first attempt at the problem it made this mistake:
"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.
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.
> Is there a clear point of departure when AI can no longer handle mathematical reasoning?
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?
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
Or at least maybe it will be a good foundation model to be fine-tuned for reasoning?
Picks up reasoning on the fly seems like wishful thinking. On the other hand in nature there also is split into people who get math and those who don’t so maybe there are 2 different ways of bootstrapping brain to be functional and luck is all we need. Anyone knows more on this?
It's just a matter of scale because when you add more floating point numbers magical things happen. The magic is called emergence, as in if you have a big enough computer then it can do anything if you prompt it the right way. As a techno-optimist I believe that thinking is simply very complicated arithmetic and by adding enough numbers we can solve any problem.
Depends a lot on how this scales though. If you need 10x as many parameters to get 1% better results for instance, then even if this works it could be impractical.
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).
Very valid point. The last papers I read on the subject conclusively show that all current networks do not hit a limit in scaling though. Bill Gates said that GPT five will not be much better than GPT four so maybe things change
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...
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.
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.
First person to submit a mechanised proof gets the payout to the address that submits the code? People can pool money into a pot? No one manages the funds individually and on a set date funds return to senders?
I actually prototyped a system like this, mostly as an exercise to learn about crypto. You can't feasibly host or verify proofs on-chain, so you need external trusted verifiers (e.g. oracles). Making sure the oracles can't front-run proof submission is a challenge. Standard formal proof system (like Lean) are sufficiently expressive, although they weren't built for this and need to be modified to make sure a proof hasn't introduced any additional axioms, as you note. The proof system also becomes a point of attack, so you'd probably want multiple, independent verifiers (which themselves have been formally proved correct). I believe these exist for some proof systems, although I'm not sure about Lean's kernel.
Ultimately, I don't think this is really practical, and investing in AI proof agents is the way to go.
> You can't feasibly host or verify proofs on-chain
I came to the same conclusion with existing systems, full on-chain verification would not be economically feasible.
But perhaps a special-purpose chain specifically made for this may not have the same limitations. Or Truebit-like oracle systems may be possible, where external verifiers can dispute other external verifier's assertions of correctness by running only the (potentially) wrong steps on-chain.
The frontrunning may be avoided by submitting hash(accountid | secret large random number | proof) first, then once that's finalized the full proof with the random number. The random number so the proof can't be brute forced from the hash. Payouts have some reasonable delay so if someone tries to frontrun the second step by intercepting the full proof and submits both steps (possibly with a varied proof) before the second step of the first person is finalized, the first person can still prove with a reference to their first step and their working proof that they were first. This still requires some thought regarding (forced) congestion in relation to the transaction cost and bounty size.
Metamath has the same problem of the system accepting new axioms anywhere, and the same $a statement being used for definitions. I have some hopes for Metamath Zero (https://github.com/digama0/mm0), which is a related system which may be able to fix this.
I think this idea is rather synergistic with proof agents. I think more people would consider developing these if enough bounties were credibly committed. It might speed up and greatly increase the number of formalized proofs.
First person to submit a mechanised proof gets the payout to the address that submits the code? People can pool money into a pot? No one manages the funds individually and on a set date funds return to senders?
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!
talking as someone who is building such a system, why would an avarage participant of the network give their own money, i dont think they would for the same reason i'm not running a bounty program with my dollars,
the only use of having it on the blockchain is rewards without using your own money (so it's economics depends on the eventual value of the coin), for that it has to be bound to the minting process, but a purely algorithmic system for determining who gets how much based on their proofs seems elusive (think of the infinite possible proofs 1+2=3, 1+3=4...), we are going for having a central authority doing the minting for proofs (as voting based on money would hardly reflect mathematical experties)
I'd like to personally put 5-10 bucks toward the solution of the Collatz conjecture, just for fun (and to see machine learning people grind their GPU-teeth on it).
No idea about the minting process, there seems to be an infinitude of possibilities.
As the parent of a young adult currently half way through their maths undergrad, this kind of fills me with foreboding.
I know that proof assistants etc have existed for quite a while now, but what with this and the murmours about OAI's Q* model, I do wonder what will happen to maths as a human endeavour - and as a enabling skill for jobs that can financially support people like my child.
I think its pretty clear that in the coming decade intelligence and cognitive labor is going to become very cheap. So your kid should develop some skills outside of that to stay competitive in the job market.
Personally i think markets will be so different from now that this question of where you'll have skills for jobs is less important than asking what will a job mean in 2040. But ok, maybe this is still a minority opinion.
I think it's pretty clear that cognitive labor will become even higher value in the future, as our tools get better and allow us to become more productive.
I wouldn't worry. What this means is that mathematics as a skill is going to be back big time, because now you can actually use it everywhere.
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.
This. Math proofs are useless in 99.99% of situations because they are far too expensive to actually use in production. Only something like AWS would use formal proofs to verify some system property for reliability.
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.
I think it's a very unfair assessment to make from these two examples. I think it's like saying Silicon Valley has been shutting down for a while and providing two examples of startups. I will say from my personal impression as someone in pure math, I disagree with this statement.
I don't know what "fair" has to do with that. These are two examples that caught my attention, and I might be wrong that this constitutes a trend. If you have data that says otherwise, please share.
I think the funding in pure math is not going down in recent years. Nor are math departments much smaller than they were say ten years ago. Otherwise I'm sure how best to give evidence of math departments not shutting down! Do I list healthy math departments?
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.
Correct - math departments are doing fine. Not quite as fine as CS departments, which get showered with piles of money and their grad students poached to make money in industry. But so long as other university departments want their students to know some combination of calculus, linear algebra, and statistics, math departments will continue humming along.
I wouldn't worry about it. We're going to need humans with specialized mathematical training in the loop.
Besides, these things have a way of surprising us. Before compilers, people wrote machine code by hand. It would have been reasonable to think that compilers would reduce the demand for programmers, but the opposite happened.
It's highly unclear to me what will happen. Probably learning math will be more accessible. But it's unclear how many humans will be involved at the forefront of math research. For example you can imagine a situation where in some parts of math large communities work in a direction guided by a few "visionaries". This sort of thing will not really happen after the commodization of theorem provers. Like instead of an advisor telling a PhD student a problem, they can just plug it in. On the other hand, in some sense the advisor and the student will be equal in the fact that the only thing you will need to do is ask questions?(last part is also speculative)
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).
I don't think research math is that accessible! Granted theoretically it's possible to just read papers and do research--and possibly it's theoretically as accessible as possible. In practice people learn better with teachers and access to experts at the research level. If this pans out, we can commoditize access to experts (or even experts).
But even in 1913 a brilliant mathematician from the middle of nowhere could access a world class mentor. I would assume that this is so much easier these days. What would stand in the way of a modern day math prodigy from getting accepted into a good program?
Or is it about making this more accessible to students who are "merely good" rather than brilliant?
Some people imagine AI will soon be a bit like being able to go to a university professor's office hours to ask questions and get detailed expert advice on any part of the undergraduate curriculum you're struggling with.
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.
> Besides, these things have a way of surprising us. Before compilers, people wrote machine code by hand. It would have been reasonable to think that compilers would reduce the demand for programmers, but the opposite happened.
I see this reasoning a lot but for me it kinda screams "correlation is not causation". As time passed and technology advanced it was simply more widely used, both on a consumer and business level. Very well may be that if we had to write machine code by hand we would need 10x more developers and a salary of $1kk/year would be average at best.
Do you really think if we get some AI agent that can write a wholly working application based on natural language specification that wouldn't significantly reduce the need for human devs?
>There isn’t a rule of economics that says better technology makes more, better jobs for horses. It sounds shockingly dumb to even say that out loud, but swap horses for humans and suddenly people think it sounds about right.
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.
> 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.
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.
In a way, all math proofs already exist. Humans just have to determine what is worth looking for and uncover them. AI will help us do the latter. But we still have to do the former ourselves.
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.
That kind of Platonism also implies that all possible computer programs already exist: because any program is merely a very large natural number, the set of which has infinite cardinality. I'm not sure how helpful this is for the practice of humans doing mathematics or software development though.
I hate to break it to you but most people with math degrees aren't doing math jobs today. The demand for such skills is low. While such an AI may displace some of the few jobs that do involve heavy math, it's likely your child will not be in that category.
How does this relate to the "IMO Grand Challenge" https://imo-grand-challenge.github.io/ ? Is this a new name / formalization, with prize money attached, or is it entirely independent? (E.g. I see Kevin Buzzard and Leonardo de Moura listed on both that page and at https://aimoprize.com/supporters)
The IMO Grand Challenge is "formal to formal" -- a solver is given the problem specified in the Lean programming language, and must produce a solution in Lean. To see more concretely what this setup might look like, check out https://github.com/dwrensha/compfiles.
The AI MO prize is "informal to informal" -- a solver is given a problem in natural language and must produce a solution in natural language.
My belief is that the best way to get to "informal to informal" is to first solve "formal to formal", but not everyone thinks so.
Do you have formal problems with formal solutions (so, you know the formalization is sufficiently complete) that cannot be found by existing (powerful) computer search techniques?
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).
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) and deciding that it's time to give this idea a boost"
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.
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.
Techno optimism is good and should be the default. I wish a16z didn’t ruin that phrase. Techno optimism should evoke Star Trek, not Silicon Valley vibes
The inevitable endpoint is the same, abundance of all resources (almost vacuously) thanks to AI/numbers/people. It is not absurd at all to believe society can be regulated and managed by a large computer with the right software. Society, after all, is just a bunch of numbers, algorithms, and arithmetic. The communists tried to do this some time ago but they just didn't have a big enough computer with the right software (AI). They were on the right track and ironically their mission will be achieved by the capitalists doing nothing other than pursuing monetary profit.
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?
Some private enterprises would undoubtedly ignore this prize, but a lot of academic researchers (including students) would be more than motivated by this prize.
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.
Maybe I’m being dumb here but isn’t the brain of one of those people the same, basically, as the model? So if a model can do X and is valued so highly, surely it’s value is pinned on a known brain that matches its skills?
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.
Two reasons:
(1) These are two different problems. Human mathematicians tend to be good at both, but there's no reason to believe (yet) that this generalization can be achieved with software.
(2) Trading has second order effects, no matter how good your algorithm is, if you apply it at any kind of scale the market reacts to it and you are left with something that doesn't work or cause large losses in the worst case.
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.
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.
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.
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.
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?
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?
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.
230 comments
[ 0.20 ms ] story [ 191 ms ] threadIt 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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
Or will he be doing it after the fact, when the questions are published.
I'm building something myself that I hope will be able to work similarly: https://aiconstrux.com
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
https://en.wikipedia.org/wiki/Grandiose_delusions
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
[1] https://github.com/hendrycks/math
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 \).
﷽!
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 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
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...
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.
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.
"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.
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?
Or at least maybe it will be a good foundation model to be fine-tuned for reasoning?
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.
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.
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.
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 idea about the minting process, there seems to be an infinitude of possibilities.
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.
(not actually serious, at least not yet)
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.
Besides, these things have a way of surprising us. Before compilers, people wrote machine code by hand. It would have been reasonable to think that compilers would reduce the demand for programmers, but the opposite happened.
I'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.
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?
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.
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.
Math shapes your mind, that’s why we learn it.
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.
I wouldn't worry too much.
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.
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).
[1] https://leandojo.org/
[2] https://arxiv.org/abs/2303.04488
> "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...
Thank for you the emphasis on openness!
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.
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.
How well do current gold medalists do in trading?
(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.
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.
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?
There are a lot of people who got burnt by FTX grants and prizes ...
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
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?
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
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.
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.
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.