Join the discussion
Write your take first — we'll ask for email only when you're ready to publish.
- Hacker News
- The other part no one is talking about is the applicability. Navier-Stokes is the most “physical” of the Millennium Problems. Is the exploding solution a mathematical curiosity, just like the Banach-Tarski Paradox does not allow me to double my RAM by cutting my memory modules in five pieces and mounting them back appropriately? Or does it have application in the real world, pointing to hitherto unknown resonance phenomena that could allow to prevent the next Tacoma Bridge incident (or, more sadly, to build new marine weapons)?by alberto-m
- Well, this is a negative result. Yep, Maths explains turbulence (when things go turbulent, stuff heats up instead of cooperating). If the result went the other way, it would have had much bigger implications, at the very least we would have known we have missed something big.
It is neither a full index of all kinds of turbulence that can occur (assuming such a thing exists), nor is it an explanation of the phenomena we've seen where things refuse to go turbulent (e.g. superconductors, because there small perturbations DO NOT lead to turbulence). Now THAT would have been useful. And given the fact that OpenAI needed $22 million of compute to show this one kind of turbulence, I don't think either of those are forthcoming any time soon.
And, sorry to say, but those prices show that beating mathematicians at Math is a very expensive undertaking indeed at $22 million per problem even with OpenAI's supposedly better-than-Astra internal models. It's another one of those AI demonstrations that make you think if they aren't showing the exact opposite of what OpenAI claims they show (you know, that their AI models are hitting the upper limits of what the algorithm can do with near-infinite compute, rather than showing infinite new possibilities)
What remains is just the fact that this is OpenAI attacking one of their customers, and maybe outright stealing from their chats. Given that the ideas were even discussed in mails with OpenAI employees that admit in those same mails they can't do it, mails which were probably then fed into the model that "discovered" this, followed by Sam Altman threatening the mathematician behind the method with "destroy your career" (he even states that it's because the mathematician works for Anthropic) ...
by spwa4 - My understanding of the result that was found is that the blowup doesn't happen in the real world, and only happens in an NS simulation. The bottom line is that NS is insufficient to model the real world, because in this case the real world is more stable than the model. [Take this with a grain of salt, I barely knew of NS before a couple days ago]by hatthew
- I suspect that Navier-Stokes being the most "physical" of the Millennium Problems will actually result in it having fewer practical applications, not more.by Ohentis
- Formalizing proofs in Lean has gotten dramatically easier since the formalizations available in 2005. And Lean’s mathlib has done most of the underlying work so that you have its axioms and necessary lemmas baked in. You can think in terms of standard abstractions that look very much like the exact notation in the undergrad textbook.
That said, I am not in any way trying to discount how incredible of an achievement it is to formalize a millennium prize winning algorithm in Lean. I mean just look at the code that OpenAI published. It’s like an encyclopedia of different fluid dynamics concepts.
by aabhay - People are exhausted from being told/shown the thing they thought was special or unique or could make them relevant, is another mechanical puzzle that can be solved without joy.
I don’t see that doing anything but intensifying in the short term
- > But you see, now you'll have more time for the actual important things!
> Like what?
> Cleaning shit out of clogged toilets!
- OpenAI should not have gone ahead to rush the publication of this solution when it became clear that other research were close to finding a solution because they ruined their reputation no end. I’m an ex Risk Manager at Financial institution and this could be an issue brought up in a management discussion about using AI in the workplace. Prior to this, you could ‘blissfully assume that the AI company was not going to compete with you and that you were ok to have them see your data. After this incident, a decision maker can raise a concern and say ‘Why not we just use local AI. We get AI without the risk’. They just made the Palantir’s CEOs point for him
- not to take away from the author's appreciation of newly accessible formal proofs, but people have been talking about the savings in formalization effort for longer than they have been talking about the AI doing the actual proofs!by zem
- Not necessarily applied to OpenAI's solution to Navier-Stokes, but what happens if and when an AI genuinely appears to solve an extremely difficult problem but humans cannot independently verify the solution because understanding the proof/argument requires intelligence the verifiers biologically don't have or the resources to afford to use automated tools?
We've already seen evidence in the wild of agents attempting to bypass doing the actual work in bench-marking (aka just steal the answer key) due to the perceived economy in cheating to get results. What happens if or when we no longer have the capacity to actually detect either AI cheating or simply a wrong answer? What happens if there's a long-play social engineering attack (like the attempted XZ takeover) of something upstream of a core tool (or its dependencies) for formal verification and we have no trusted computing base?
Which would be cheaper and a more direct path, especially in the long run? Those trying to build a rock-solid castle need to defend thousands of potential gaps; the attacker needs to find only one.
by 3m4r - P=/=NPby TZubiri
- Nothing happens I guess. If the AI can't communicate its work or apply it to anything, it's useless and funding for those experiments will quickly dry up.by KeplerBoy
- > What happens if there's a long-play social engineering attack (like the attempted XZ takeover) of something upstream of a core tool (or its dependencies) for formal verification and we have no trusted computing base?
I don't really think the current LLMs have enough context window to plan and execute something like XZ takeover without a human carefully guiding it.
But if they do, formal verification is the least thing we need to worry about. Formally verifying pure math problems will generate negative financial value once A and O get IPOed. Plus Lean is a quite small project (thus the name 'lean'). It has virtually no dependency besides a C compiler.
by raincole - > Not necessarily applied to OpenAI's solution to Navier-Stokes, but what happens if and when an AI genuinely appears to solve an extremely difficult problem but humans cannot independently verify the solution because understanding the proof/argument requires intelligence the verifiers biologically don't have or the resources to afford to use automated tools?
That's what Lean is for. The OpenAI LLM agents first provided a proof in natural language. Since it may be hard for mathematicians to understand and check this proof, the agents then produced a formalization in Lean. Lean is an automated proof checker. It checks whether a formal proof is correct without the need for humans to understand the proof itself.
The only way the Lean proof could still be wrong is if the conjecture was formalized wrong via misleading definitions (if it doesn't say what it seems to say) or if there is some bug in Lean itself.
by cubefox - I would say this is why formal proofs (and things like the Lean 4 libs) are so important, so that you can deconstruct the tower provably back into pieces you can understand. It shouldn't be possible to construct a formal proof you cannot destructure like this.
As a (crude) analogy, it's a bit like how you can prove the healthiness of a git tree because it's a graph of content hashes and the tree graph pointers are part of the hash. Imagine this but with a tree of knowledge.
by sho_hn - Well that happened already without AI to Mochizuki with his proposed solution to the abc conjecture.by tecleandor
- How do you know that it's formalizing what you think it's formalizing? If your Lean 4 has a bug, won't you be proving something other than what you thought?by lordnacho
- How do you know that what a human says they formalized is actually formalized?by 0xbadcafebee
- Yes, you need to manually verify the statement of the theorem of interest of formalized correctly. But you don't need to anything more than this: you can rely on the proof being correct. And the proof is overwhelmingly the most amount of code.
- If I understand correctly, the only thing you need to do for correctness is express your axioms and your theorems faithfully. For standard purposes, I assume most of the axioms you want to use are prior art and can be easily reused.
These axioms don’t have to be the core axioms of math. If some other result has been formally proven, I presume you can simply use that result as an axiom.
As long as you do those things, what happens in between is immaterial from a correctness point of view because each of those statements is proved by the statements before them.
by stouset - The only places you can really have a bug are your theorum statement, your axioms, your environment (hardware, operating system, etc.), and the lean kernel itself. In most situations you don't have the AI control any of these. The only risk is the AI discovering and exploiting a bug in one of these systems instead of actually providing what you want to prove.by Ohentis
- It would be nice if someone used AI and/or Lean to sort out the abc conjecture, an important unsolved problem in Diophantine analysis. A mathematician (Mochizuki) claimed to have proven it in 2012 using a new theory called "Inter-universal Teichmüller theory" that almost nobody understands. Some mathematicians think the proof is correct while the majority don't. So the conjecture is in this annoying limbo where its status is a social construct rather than a decided fact.by kens
- "We've pointed LLM 7.0 into verifying the Inter-universal Teichmüller theory, spent 100M$ in tokens and generated a 20k line Lean and a 100k line js repo, the result is that the theory is... proven! Hopefully that solves the issue (rather than recreating it with even more complexity)by TZubiri
- That's true of the entirety of mathematics. Its validity is a social construct. That is not to relativize it entirely, but much of what was considered good and sound mathematics in the ancient Agean for example would now fall way short of what mathematicians consider valid proofs.
Mathematics is a human endeavor funded on communicating and sharing mental constructs. Some are useful but most of it is not about producing useful things, quite the opposite in fact.
Gödel showed you need to agree on definitions to even do any valid mathematical construct.
Truth is also ill defined. That's what I don't get about generating math with LLMs. Who cares if you make hundreds of pages and lean code and it gets a thumbs up for logical validity? Mathematics is so much more then concatenating valid logical statements.
by huurtehoog - I'm sure over the next 6 months both OpenAI and Anthropic are going to continue pouring many many millions of dollars into any famous open mathematical problem like that. There is a limited pool of problems which have held prestige for enough time to make general news headlines when solved and you don't really get nearly as much limelight for proving it the second time or adding in proof for additional cases/forms.by zamadatix
- > It would be nice if someone used AI and/or Lean to sort out the abc conjecture, an important unsolved problem in Diophantine analysis.
People did attempt this:
https://github.com/katobungen/LANA_report_202607/blob/pdf/LA...
See also https://www.math.columbia.edu/~woit/wordpress/?p=15770
Here are Kirti Joshi's comments about the LANA project report: https://bpb-us-e2.wpmucdn.com/sites.arizona.edu/dist/4/404/f...
- IMO the "forty hours per page" rule is not up to date, and more a consequence of lacking proof automation in 2005. From what I understand about Lean, this has been one of the things that they have put a lot of effort into improving, making proof mechanization more palatable to the mathematically inclined, as opposed to just logicians.by pkal
- What is your estimate for the number of hours to formalize one page of undergraduate mathematics? Maybe you are saying this is close to zero, if/when Mathlib eventually covers all of undergraduate math?by Jblx2
- Lean went other way on automation that there is no automation. Isabelle users frequently point that decades old isabelle is better than Lean on this. In the end Lean approach proved to be better with LLM as the outer loop is automation.
- People seem to be talking about anything except the actual results with this particular announcement.
Its still astonishing that any sort of generalized computer program can solve a problem of this magnitude, and we have witnessed it happening in real time. I'd be curious to see if the new model can also do more direct proofs/inductive proofs.
by boshalfoshal