[deleted]
OpenAI’s Navier-Stokes release included a Lean 4 formal proof
71–80 of 129 posts
Re: OpenAI’s Navier-Stokes release included a Lean 4 formal proof
#72Earlier quoted context omitted.
> But you see, now you'll have more time for the actual important things! > Like what? > Cleaning shit out of clogged toilets!
How about figuring out how to turn all of our shit into usable fertilizer?
This is surprisingly apt to me. Fertilizer is apparently one of the fundamental geopolitical dependencies on capital and access to petrochemicals. Solving fertilizer would unlock a huge amount of human potential in the Global South.
Re: OpenAI’s Navier-Stokes release included a Lean 4 formal proof
#73Earlier quoted context omitted.
It also needs to be said: The amount of compute that went into this is something. From some estimates I've seen, the compute cost alone would be around $10m, +/- As a reference, for that kind of money one could put together a research group of 20-25 researchers, and keep them salaried for 5 years. So while it is impressive, absolutely no doubt there, the SOTA access is so expensive that it is sort of unobtanium. Luck…
Once we have an existence proof of a particular technology, it doesn't take long for it to become economically viable and proliferate. And for something as useful as this, theres a strong economic incentive to get it to be as cheap and accessible as possible. Maybe not today, but certainly in a couple years I can imagine this level of intelligence being accessible to someone with a $20/mo plan, or even a free plan.
I remember being blown away when a then-unreleased version of GPT 5 took gold at the International Math Olympiad. Now I can run a model at home that can do that. We are more fortunate to have these tools than almost anyone is willing to acknowledge.
Re: OpenAI’s Navier-Stokes release included a Lean 4 formal proof
#74Not 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…
[dead]
Re: OpenAI’s Navier-Stokes release included a Lean 4 formal proof
#75The part that most stood out to me was where Sama said, “we read last week about people trying to solve Millenium problems and so gave it a shot.” One week of work on a whim gives us a math breakthrough. Crazy.
Re: OpenAI’s Navier-Stokes release included a Lean 4 formal proof
#76How 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?
How do you know that what a human says they formalized is actually formalized?
Re: OpenAI’s Navier-Stokes release included a Lean 4 formal proof
#77Not 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…
> 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.
Re: OpenAI’s Navier-Stokes release included a Lean 4 formal proof
#78The part that most stood out to me was where Sama said, “we read last week about people trying to solve Millenium problems and so gave it a shot.” One week of work on a whim gives us a math breakthrough. Crazy.
Casual? casual dice, lo que hizo OpenAI fue plagiar el arduo trabajo de dos investigadores. Plagian y mienten! (Las BigTech) plagian todo lo que pillan y mas! ;)
Re: OpenAI’s Navier-Stokes release included a Lean 4 formal proof
#79People 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.
Heck, it’s even astonishing that any sort of generalized computer program could even verify a proof of this magnitude that hasn’t already been codified in a formal verification language. If, and it’s unclear that we’ll ever get the full story, they did draw inspiration from training on (or even directly accessing) rough notes that had been provided by another researcher in prose… the fact that it could leap so rapidl…
Then, of course, one must verify that the verification code is valid, or the purpose of verification is more or less moot.
Re: OpenAI’s Navier-Stokes release included a Lean 4 formal proof
#80Regarding automatic formalization of proofs using AI, how do we know the formalization doesn't contain errors?