Take something like Fermat's last theorem - I'd be curious to hear of any use of the result itself, but there was a massive amount of new mathematics generated by those working on it, whether ultimately successful or not.
These AI math proofs are interesting testament to the power of reinforcement learning applied to math, obviously reflecting the axiomatic self-consistent nature of math itself, but it doesn't seem they have the same value as a humans working on these problems since they are using known math to solve them rather than inventing anything new.
However, it would still be interesting to analyze the LLM lines of reasoning that lead to any of these results, since there may be value there even if no new math, just as human Go players have found value in analyzing computer Go.
Still, as Demis Hassabis has himself said, the real goal with AI is discovery and creativity - you want to create the thing that could design the game of Go in the first place, not just play it. Similarly with math, while there is interest in seeing an AI "play math" using the rules of the game, what would be of much more interest is the AI that can create new math, in the same way as Andrew Wiles did while proving Fermat's last theorem.
Isn't a new proof new math? If not, what qualifies as new math?
An interesting thought experiment would be: assuming AI can solve any given problem (or prove it's undecidable), and thus that the "proving" activity becomes trivialized, what's the interesting part that remains? Can we work on "refactoring" mathematics to make it more intuitive? More "powerful" in some sense? What are other refactorings that are worth exploring?
It may actually be a negative, rather than a positive, for AI to have solved these problems.
If humans had continued to work on these problems, then its quite possible they may have invented new math along the way and benefited the field. Now that the problems are solved, in one manner, I would assume that the level of human interest in them is much diminished, and the likelihood of these problems generating the same benefit for mathematics has diminished. Erdos chose his problems precisely because he thought they could advance the field.
AI itself does not appear to have benefited from solving these problems - they are hard for a human but apparently fairly easy for an AI. We don't just have one result here, proven after great labor, but 10 (with more results rumored to be withheld), with the effort/cost to generate them reported to be low.
The temptation to announce AI solutions to problems that are hard for humans, easy for AI, may be hard to resist, but perhaps there would be more benefit to be had to leave the hard for human problems for humans to solve, and be more impressed when AI solves problems that are hard for AI.
As Hans Moravec noted "What's easy for humans is hard for computers, and what's hard for humans is easy for computers", and while AI is trying to make inroads into that, it still remains fundamentally true.
Or another angle. Given that, from my amateur understanding, a lot of these problems are proof by counter-example, could you not argue that at least AI eliminates low hanging fruit and more important problems can gain focus.
Of course, I could equally argue that the low hanging fruit is needed to train up mathematicians.
So yeah, in the end, I don't know. But am pretty certain that AI is not going to be limited by these sort of proofs for much longer.
Math is an incredibly broad field. I mean, you don't expect a traffic engineer to understand anything about nuclear reactors, do you? Yet, they are all 'career engineers'.
I might have overstated a bit, but by 9th grade (15 year old) this is what was taught to us back then.
What you learned, was it more like:
1. "You need to slow down neutrons so they can react"
or 2. "Here's the graphs of how the neutron absorption and scattering cross sections vary with neutron temperature for H-1, H-2, H-3, Be-9, C-12, O-16, Fe-54, Fe-56, Fe-57, U-233, U-235, U-238, Pu-239, …"
If it was the former, you didn't learn "nuclear engineering".
(which is a simplification in itself, but that's best left until 2nd-3rd year in uni)
But for general understanding, .. there is stuff that slows neutrons. some is more effective, some less. There is also activation. It is why tanks and ifvs were lined with polyethylene or similar on the inside back in cold war - it had lots of hydrogen. But for controlling a power plant that is not enough - why?
and then we answer why.
It turns out that the "more CO2 = more warmer" model is hilariously simplified, and the real modelling gets into the weeds to put it mildly! There's a NASA database of the super-high-resolution absorption and emission spectra of every isotopic combination of every common molecule and ions, excited states, and more! It turns out that most of the forcing is determined by the behaviour of the upper atmosphere at high latitudes where the air is so thin that exotic excited states can persist for appreciable durations, and are made in large amounts by absorption of UV light. The "glancing angle" of the sunlight near the poles also means that even minor constituents participate in the exchange of IR radiation. Then, then, the simulation has to be run in many thin slices because air is so opaque to IR radiation that it bounces many times on the way up and down, and of course, the isotopic mixes (and excited fractions) are inconsistent between layers.
An insanely complex supercomputer model is required to come up with even a rough estimate of the actual warming.
Only those who try to maximize profits while skirting the risk of a revolt care whether global average temperature will be 1.2 or 1.8K above pre-industrial average in ten years. For the rest it's already too warm, the damage is already plainly visible.
We don't need better models to predict future warming; we dragged our feet long enough that we can now look at historic data to see where it's going.
Newton's laws of motions are not hard. Making a rocket that doesn't kill the occupant, is.
For the 2026 version of me out there, please ignore. It is nerd posturing, and as real as the boomers at your gym claiming to have benched 225/315/405 in high school, despite having terrible form while doing 185.
>And then -- the kicker -- something that I personally spent a couple years on in grad school, leading to some of my proudest work: quantum parallel repetition theorems
...
>Is there some broader context or theory within which this would've been the obvious thing to do? What other results can be proven using these techniques? What is it telling us about quantum information or operator theory? I have no idea
https://bsky.app/profile/henryyuen.bsky.social/post/3ms2jpch...
That guy has been featured in quantamag too, btw
I saw another expert on Ehrhart express their bafflement (but I can't find that link now)
PP (actually the "broad career mathematicians" themselves) were being slightly disingenuous... But the specific domain experts seem to be understating how much over their head it actually was. We're in totally unknown territory here..
we can however be optimistic, oddly. If you believe Feynman when he says that you can't explain to a child something you don't understand.. then we can see that ChatGPT has no idea of just what it has done!
(Steel Manning:
1. maybe any chatbot would need 1000x more tokens than were used to arrive at the result to understand it to its own satisfaction.
2. It's possible that Einstein did not fully understand General Relativity
Why would that be optimistic? Seems like the pessimistic reading to me, if anything. Or are you having a bout of Schadenfreude?
Compare the various summaries that humans have written on the Jacobian counterexample, to the chat logs that were archived.
I'm not guessing that they aren't working on this aspect or that chatbots won't be able to do it in the futute. It just seems that we do have an advantage for now.
Since at least 2014, which was my first brush with the phenomenon when someone published a 13GB proof [0].
The consensus is that such a proof is potentially illuminating, though further work is likely required. If for instance, conjecture A is true if and only if conjectures B & C are true, and B is proven false through one of these such proofs, then we can see that A is also false given that we accept the disproof of B.
Though, the sense is that further work is likely required because it is easy to see that further work along the same direction, or in directions depending on the proof will be hard or impossible if there are not enough humans or agents that are capable of understanding and utilizing the proof. Making it 'more elegant' will increase it's utility despite not proving anything new.
This is adjacent to all of the work done to create multiple proofs using different techniques. Having the same information (that X is so) in different languages (algebraic, geometric, via harmonic analysis, etc) allows for researchers not familiar with the original technique to participate in further research.
[0] https://www.newscientist.com/article/1997488-wikipedia-size-...
Example: https://nitter.poast.org/henryquantum/status/208362369543662...
Seems like a disservice to the community that openai put so little effort into producing good writeups...
Then again, this would require them to actually care about the mathematics.
Because it's math, it's all mysterious and genuinely impressive, but in the end, if no human cares about it (apart from attention grabbing "it's so over" tweets and articles), does it really matter?
I'm not sure that a problem being famous, or hard for a human, is the same as it being important.
Take Fermat's last theorem as an example - was a proof of it ever considered to be, then or now, consequential, or was it the Paris Hilton of problems - famous for being famous? A problem whose legend grew because it it so simple to state, with the challenge that there might be a simple proof, and that turned out to be so difficult to solve that it therefore became prestigious to do so?
Except OpenAI isn't showing any upvotes.
One open question is whether these machine solutions to these problems will act as springboards to future research, either when given to human mathematicians, or when used to train future machine models.
Which one were you referring to?
Unless you want to be the guy in the 19th century making fun of Boole algebra for having no practical use. You might be right, but not for long.
even the ZMachine it's an astounding example of running virtual machines on 8 bit machines 20 years earlier than Java.
P.S. Couldn't resist :p
Is it dense or MoE?
It's a good model Sir!
In all serious "I don't understand any of this it's way over my head."
It does and that's what's happening.
So it's just a matter of combinatorics.
The way the chess world adapted this was initially to try to understand the machine. After all chess, like math, is complete information - so you can easily see the computers 'thoughts' in terms of the exact moves its saying are best in a variation and how it might respond to any other idea. But it quickly became clear that this wasn't working so well.
Players would regularly get positions that the computer says 'and black wins' and then proceed to lose it convincingly, simply because the positions were so extremely weird and difficult to play that even if it might be technically winning, it's the sort of position where you're walking a fine line with lots of complex moves to find. Humans aren't computers and even the best of us can't play like one in weird positions.
Now a days they're taken more in balance. The computer's evaluation of a position is probably about as good as you can get, but playability matters much more in practical terms. Knowing the eval of a position doesn't really matter if you don't understand the position. Knowing the answer can help with understanding (for instance computers have radically reshaped and improved human understanding of space in chess as we noticed computers obsessing over it) but I think the days of 'oh the computer says it's winning, so I should be able to take it from here' are near to gone.
A lot of people were super hyped about OpenAI's 10 discoveries, but I still don't understand what they mean, and even if I did, what are the implications.
Like, what are non-sofic groups, and what follows from the conclusion that they exist?
I mean in the sense that quantum mechanics might make my head spin, but it's because of that that we have stuff like semiconductors, which have been one of the most significant discoveries.
The Fourier transform is one of the reasons we have fast telecommunications and radars.
What practical things are possible or might be possible due to these results?
Not much, they're all fairly minor problems that have been solved, of ~entirely niche academic interest. It's so far more just that AI _can_ solve novel math problems, ones that humans didn't accidentally train the answer in and it just spit it back out.
I have no idea what it's about because im not in algebra but the algebraists say its a big thing.
Huh?
Mathematics is an extremely wide subject, it's perfectly normal even for two professional mathematicians not to understand each other's work. Have you considered that maybe they just don't work in that area?
Are you implying OpenAI's paper (which was, by the way, edited by humans and provided Lean certificates for most of the proofs) is actually gibberish? That's flat-earth levels of conspiracy.
This is not new nor unique. There is plenty of research, especially in math, which can really only be understood by a few people in the entire world. It is not uncommon for a proof to be presented by a mathematician which, initially, is only understood to that mathematician, and it can take a long time for even another mathematician who is an expert in the same field to be able to confidentially say they understood it.
>I saw lots of career research mathematicians say things mostly along the lines of “I don’t understand any of this it’s way over my head”.
This is meaningless in a vacuum. If you give a novel proof in some niche subfield of topology to a competent mathematics researcher who focuses in number theory, they'd say the same thing regardless of if a human or machine wrote the proof. A bunch of "career mathematicians" on Twitter proclaiming this doesn't mean anything other than these people aren't currently equipped to understand the contents of the proofs. That's fine and normal, but the idea that anybody with a PhD in Math should be able to pick up one of these proofs and give it a skim and be able to say, "ahh, yes, quite clever, it seems so obvious in retrospect," is absurd. That's not how this kind of research works.
>Are we ready to just let go of our intellectual faculties and give them to a giant supercomputer nobody understands?
Nobody is blindly accepting these proofs as valid. ChatGPT isn't spitting out a wall of text and proclaiming that they've solved a previously unsolved math problem while everyone is saying, "well if an LLM says it, it must be true!" lol
These proofs are being checked by automated systems (which have been in-use well before LLMs have existed) as well as being checked over by actual experts who are actually capable of (and motivated to) verifying these proofs. But that work still isn't done. There's enough evidence that these companies are confident in saying these proofs are correct, but there's going to be a lot of ongoing work from people to continue to verify and, more importantly, understand these proofs. It's literally some of these people's full-time jobs to do this.
>How do we tell truth from fiction?
When was the last time you verified even a classical, relatively simple mathematical assertion? How often are you just relying on a larger system of experts to ensure that we're not just blindly accepting fiction as truth?
That's not to try to stick it to you personally, but it's just highlight that there's an entire system in-place here that you're not aware of and that you don't have an understanding of that is working just fine including in this context. Real mathematicians aren't going to lazily start letting OpenAI assert whatever they want about their products solving these kinds of problems without heavy scrutiny.
It is, provably: per Curry–Howard correspondence, any program you write is a proof of a theorem, and it is indeed mathematically meaningless.
I can't tell if xkcd #435 is still true, or if math is just as mushy as everything else seems to be. When a math proof can only be understood by a handful of people, what does that mean about that proof? I think the LLMs are pushing a problem that existed already and pushing it further.
The process is very, very faintly similar to running a typechecker over your software sources.
They don't understand the math either.
You are right that Lean isn't great in this respect, and people are working on proof formalisations that are less prone to bugs.
Making things understandable is mathematics, and more generally a kind of intelligence, and is crucial to continued progress. You couldn't use algebraic geometry to disprove a conjecture if people hadn't organized (what could have been just) a pile of random observations into something called algebraic geometry.
Historically LLMs have done best where it's possible to train using an objectively verifiable reward function. Computer programs are pretty good on this front and so are Lean proofs. (Of course, they don't only do things you can RLVR heavily, but those have progressed fastest.) Not sure where 'making mathematical knowledge more understandable' falls on that spectrum.
Understandability isn't only important for advanced math. Keeping computer programs from becoming a mess is a challenge in high-level organization too, and the chat with the user is an explanation task. If you look online at what people say about large LLM-built codebases (SlopCodeBench is a neat effort to make make it concrete, but common wisdom seems to mostly agree on the general problem) and chatbot prose, I don't think everyone considers those solved problems!
It's hard to tell how thoroughly the labs grasp and care about this at an organization-wide level. I'm sure at least some maybe-results exist inside labs but haven't been published because the humans couldn't verify them and didn't want to be embarrassed with a false result. (Maybe also why counterexamples are a lot of the first results published: often simple to verify, even if hard to obtain.) A good sign would be if results in a few months come out more like what mathematicians consider well-written papers explaining results in a more intuitive way, fewer shocking announcements of bare counterexamples in tweets. It's probably a slow climb to get there.
An unsettling number of people do seem to be more than ready for this. In fact I'd say they seem almost gleeful about it. Thinking is hard and they don't seem to like doing it!
I mean, arguably the development of LLMs matches that description.
Theoretical science isn't about usefulness per se, but knowledge and understanding for its own sake, so a better way to say this is to point out that you only benefit in such cases if you understand things yourself. If understanding is the goal - which it is in the case of true theory - then the only way to attain that goal is to actually attain understanding. What good is it if an LLM produces a valid proof, but no one grasps it? This isn't like digging a ditch where it doesn't matter who does it or how he does it as long as you have a ditch. Here, the ditch is knowledge, as it were.
What are the odds that this random FOSS project has solved the problem of building software and nobody noticed. Close to 0. Don't confuse accidental complexity for transcendental depth.
Isn't that what people from more practical sciences said about math anyways?
All math is eventually applied math.
Are we missing the forest for the trees here? If a math problem falls in the forest but nobody is around to understand it does it make a sound?
How can we possibly make use of these breakthroughs if we don’t understand them? How could we ever make anything useful with them?
Are we ready to just let go of our intellectual faculties and give them to a giant supercomputer nobody understands? How do we tell truth from fiction?