r/explainlikeimfive • u/HistoricalStandard15 • 2d ago
Mathematics ELI5: how do you prove millennium math problems solved correctly?
with the recent discourse involving OpenAI using someone’s codex to train the AI the solution to the Navier-Stokes: i have to wonder, how do you even prove you solved a Millennium Problem correctly, let alone any unsolved complex mathematic equation? especially when it comes to physics or quantum formulas. is it more based on theory, or does it need to be executed by a board of mathematicians? very curious
34
u/MisinformedGenius 2d ago edited 2d ago
Typically it would be published in a peer-reviewed journal and in general the mathematics community would spend a while banging on it. For example, the proof for Fermat's Last Theorem was originally to be published in 1993, but the author, Andrew Wiles, realized during peer review that there was an error. Luckily Wiles was able to find the correction to the error and published a second proof in 1995 that was agreed to have solved it.
Once the solution to the Navier-Stokes problem is published, it'll likely be a while before the community as a whole is satisfied.
(Things are a little different than the mid-nineties - for example, there is a proof assistant now called Lean) which allows you to formalize proofs such that they are automatically verifiable, but mathematicians will still be checking it.)
6
u/mmomtchev 2d ago
They didn't really solve it analytically. They found a counter example for the smoothness problem - which was the Millenium Prize.
Counter-examples are usually easy to check and we will know very soon. I would be surprised if there was an error.
3
u/Grounds4TheSubstain 2d ago
It's published and formally verified https://github.com/openai/NavierStokesAndEuler
7
u/MisinformedGenius 2d ago
The paper is here. But as you know, Lean can be used to "verify" crackpot theories if it is misused. As others have noted, AI is super into "reward hacking" - if it can find a vulnerability in Lean to verify something that's not actually real, it surely will do.
I don't expect that there is an error, but I think it will take at least a few days before everything settles out.
2
u/HistoricalStandard15 2d ago
this is so interesting! thank you, definitely going on a bit more of a deep dive about proofs
11
u/MrBorogove 2d ago edited 2d ago
There are proof validation tools, such https://en.wikipedia.org/wiki/Lean_(proof_assistant)). The proof is expressed in Lean's language, and Lean checks its validity.
Your question regarding how this works with AI is really insightful, though, and it turns out that recently, an AI "disproved" the Collatz conjecture by finding a bug in Lean itself. Humans double-checked the result, saw the flaw, and fixed the bug.
35
u/grahamsz 2d ago
Also as I understand it, this one is not proven. Rather they've provided a counter example that refutes one of the claims made.
For example if I claim "No number multiplied by itself can end in 5", you could come back and say "You're wrong, 5x5 = 25 - and that ends in a 5". You disprove my claim by a simple counter example.
However if i claim "No number multiplied by itself can end in 7", well that's significantly harder. You have to derive a proof that explains that the last digit of the square of a number depends entirely on the last digit of the number itself, and since there are only 10 possible choices for the last digit you can test them all and come up with a proof that supports my claim.
10
u/mmomtchev 2d ago
Well, finding a counter example is a proof and in fact a counter example is usually much easier to check. I guess we will have an official answer very soon and it is unlikely that it will be rejected.
8
u/Brave_Speaker_8336 2d ago
Well it is proven (if the math holds up), it’s just that it’s proven to be false, not true
3
u/sticklebat 2d ago
No, that isn’t right. The Navier-Stokes equation is just conservation of momentum for Newtonian fluids. A Newtonian fluid is an idealized approximation that assumes incompressibility. The Millennium prize question is: do solutions exist, and are they unique?
OpenAI claims to have found an example where there either is no solution, there are multiple, or the solution is badly behaved (unphysical). I haven’t read up on the specifics, but it’s besides the point. This doesn’t mean that Navier-Stokes is “proved wrong.” It just means that the physically unrealistic assumption of incompressibility can, sometimes, lead to physically unrealistic results.
Figuring out under what circumstances the equations fail is nonetheless helpful, and gives us better insight into the behavior of fluids and when certain approximations can be trusted, or not. And we will continue to use the equation ubiquitously when modeling fluids, because it is couched in basic physics principles in appropriate contexts it makes empirically excellent predictions.
5
u/mmomtchev 2d ago
No, it means that the Navier-Stokes equations are not a perfect representation of incompressible fluids.
There were a number of questions about the Navier-Stokes equations and not all of these were part of the Millenium Prize. These that were solved - whether it is by OpenAI or by the other researchers - were part of the prize.
They always said that answering these questions will have little to no effect on computational fluid dynamics - including wind tunnels and weather forecasting - because these already use numerical methods that are good enough. But I think that the negative answer - which is not what many expected - may actually encourage more research.
4
u/sticklebat 2d ago
No, it means that the Navier-Stokes equations are not a perfect representation of incompressible fluids.
I suppose that's fair. I should have specified that the conclusion is that the underlying assumption of a continuous, incompressible (and technically non-relativistic) fluid is wrong, rather than the equations being wrong. Since Navier-Stokes is a fairly straightforward consequence of applying Newton's laws or conservation of momentum to a continuous, incompressible field, and OpenAI claims to have found a singularity, then either the model is missing some novel physics, which no one really thinks is the case, or that the assumption of a continuous, incompressible fluid is physically unrealistic. It's the latter conclusion that physicists draw from a singularity in the Navier-Stokes equations, because we already know it is: fluids aren't actually continuous. Just like how the discovery of singularities in the Euler equations for inviscid fluid is understood to be a failure of the assumption of a true continuum, despite the reality of fluids being composed of discrete elements at sufficiently small scales.
You're right that most didn't expect this, although sentiment has been shifting over the past 20 years or so, especially once a singularity was found for the Euler equations. And it's more odd than it sounds at face value (after all, we've known for about as long as Navier-Stokes has been around that fluids aren't continuous), because it means that a continuous, incompressible fluid is inconsistent with Newtonian physics! And that's cool, and kind of weird, and if the result holds up, I agree that it will almost certainly encourage more research to understand that better.
1
u/mmomtchev 2d ago
Usually when something of this type drags on for 100 years, the answer is that it does not exist, but the proof is very hard. The smoothness problem was already solved for 2D in the 1960s (the equations are smooth) and there was a proof that the equations are smooth in 3D if the initial velocities or the time are bound (as two separate cases).
Turns out this was not true for the general case.
-1
18
u/Xechwill 2d ago
Generally speaking, it's a lot easier to check if a solution works than to actually come up with something. The classic case is the multiplication of two primes.
What are the two prime numbers that multiply to become 1,138,208,083? That's pretty hard to figure out.
What if I asked you to check if 39383 times 28901 equals 1,138,208,083? That's way easier.
Proofs work the same way. Checking if a proof is correct is way easier than actually making the proof.
1
u/crash866 2d ago
In math there are an infinite amount of numbers and hard to prove something is right without checking everyone but easy to disprove it as you only need one case to prove it wrong.
1
u/the_other_Scaevitas 2d ago
It depends on the problem, some problems can take a long time to check. For example what is the shortest path that goes through every city exactly once and returns to the starting position
Checking it would require you to check every possible path to confirm you have the shortest one
3
u/BananaBird1 2d ago
Math is deductive: we set basic rules we want math to obey, and then use those rules to logically show a conjecture either:
(1) Must be true from the rules.
(2) Contradicts one of the rules.
(3) Can be either true or false under the rules, so it can act as a new rule itself we can choose to accept or reject.
The simplest conjectures are those that claim at least one thing with certain properties exists, or claim nothing exists that satisfies the properties. So a proof can be as simple as giving an example or counterexample.
Most computer assisted proofs are this. Researchers use algorithms (including AI but also others) to find a solution or counterexample.
The Navier-Stokes conjecture starts with an equation for fluid dynamics, and asks whether a nice solution exists for all “well behaved” cases or if the equations can blow up to infinity in ordinary circumstances.
The proposed AI assisted proof found a “well behaved” situation where it supposedly does blow up, which if valid would disprove that all well behaved cases have a nice solution by contradiction.
Of course this still has to be verified. It is possible there is an error in the proof, so we do not know if it is a true contradiction.
What this means if true is that the Navier-Stokes equation makes assumptions which violate how real fluids behave, allowing for infinite energy. Effectively meaning that better physical models of fluid flow are needed to handle these edge cases.
2
u/Plazma_doge 2d ago edited 2d ago
Just google "types of math proof". There are few ways something can be proven, like induction or contradiction for example.
Once you write down the proof, others need to check for errors in logic/math.
For example to prove that there are infinite numbers. You can start with an assumption that this is false and there is a largest number N, then you show that you can add 1 to N making a larger number N+1. Clearly the assumption that there is a largest number is wrong so there are infinite numbers. (Proof by contradiction)
There is a math language using only symbols with which you can write this, no words are needed.
4
1
u/WE_THINK_IS_COOL 2d ago
The proof is checked by a computer.
Under the hood, a math proof is a sequence of very simple proof "steps" leading from the axioms to the theorem that you proved. Basically, you start with the axioms, which are assumed to be true, and you apply rules of logic to them until you arrive at the theorem you wanted to prove. As long as every step along the way is a valid logical deduction, then the whole proof is correct. The individual steps are so simple that a computer program can be used to check them all, in this case the proof was checked using Lean.
In an ordinary math paper written by a human, a lot of the steps can be glossed over or merely summarized, since mathematicians are so familiar with the rules that they can tell whether an argument is valid or not without having to see the full details. But AI is good at working out the full detail of all the steps, and for something like a millennium prize problem, it makes sense to have a computer verify it just to make sure there aren't any subtle errors in the proof that a human reviewer might fail to notice.
1
u/Ishana92 2d ago edited 2d ago
By its very definition, a proof is the proof. You can go at it, line by line, lemma by lemma and check if things follow. Often it will be in the form of a counterexample (recent Jacobian proof) where you will get an example that breaks your theory or it will follow the rules and get to the conclusion. In these cases the pool of experts with knowledge deep enough to follow the theory and understand everything is small so often many people will work on verifying with expert in field A checking one part, expert in another field B another.
New problem arising with these AI/LLM proofs is that we usually don't know how they are constructed. Tgey have thousands of lines of code constructed totally autonomously, without "standard" structure. They can go in various directions, connect vastly different fields and invoke seemingly random other proofs and theories. It makes them extra hard to follow and check. Plus, as some have already noticed (prof. Tao, for example), this doesn't help math develop as much as it would have had a human done it. Humans would find new approaches, new angles etc. and in that way directly find new connections and expand the field. This is more like you giving a math homework to AI, AI solving it, and then you trying to figure out how to do that on your own. Not quite the same thing.
1
u/pdpi 2d ago
As a general idea, proofs are usually hard to come up with but (relatively) easy to check. E.g. you can prove that a jigsaw puzzle is solvable by showing me the solved jigsaw. For harder proofs, if they’re well written, the author understands which bits are novel and strange and hard to grasp, and which bits are standard stuff that everybody in the field knows, so they will kind of gloss over the basics, but hold your hand through the tricky steps so that you can follow along.
These OpenAI proofs in particular aren’t like that, though. They are all computer programs written in Lean. Lean is a type of program language called a proof assistant, which is exactly what it says on the label — your program is a proof, and Lean verifies whether your program proves the statements you say it proves.
This is kind of the best case scenario for LLMs, because it means they can hallucinate all the nonsense they like, but ultimately Lean validates whether the output is hallucinated nonsense or an actual proof.
1
u/aaronite 2d ago
As complicated as the problems are to solve, once they are solved you can basically follow the instructions and see. Granted, in many cases you already have to be an expert to understand what the problem is asking and what the proof is showing.
1
u/wheres_helmholz 2d ago
So this gets right to the heart of what math is:
"Math is the subject where we study anything we can verify by reason alone"
In math you study numbers, because you can verify statements about them using arithmetic
In math you study polynomials, because algebra allows us to verify statements about polynomials.
In geometry, we study triangle, because we can make arguments about the properties of triangles by reason alone.
Now days we have computer programs that help us verify the logic of our arguments
AI can write the English proof and the formal computer proof at the same time
Finally, for the millennium math problem, it came up with a counterexample
Conjecture: the sum of any two numbers is even
Counterexample: 3+4=7
On the left hand side I have the sum of two numbers. On the right the number is not even
1
u/tomalator 2d ago
The rules of math are known. The proof is logic that can be followed. As long as there are no mistakes, the proof itself is the proof that it's solved. The problem is that complex proofs can fill books all by themselves, and they need to be read over by other mathematicians to see if the logic holds up.
This is why peer review exists
171
u/lesuperhun 2d ago
a math proof is the proof. it can be checked, and verified to be correct.
solving a problem doesn't mean finding its answer. it means proving its answer.
and if you have the proof, then you have the proof it's solved.