How An AI math breakthrough ignited a controversy • Hacker News Board

Re: How An AI math breakthrough ignited a controversy

#241

Post by jibal » Thu, Sep 10, 2026, 12:46 AM UTC

bananaflag wrote: post #15

jibal wrote: post #4

> OpenAI, meanwhile, says its experience with Navier-Stokes could open the door to solving puzzles with more practical relevance. “We are now able to spend millions of dollars on a problem that we really care about and that really matters: developing new materials, finding cures to diseases,” Bubeck said. “All of those things that we have been talking about for a long time—now they seem to be at our fingertips.” Eh?…

Yes it is they all require intelligence. Navier Stokes is a test of how high the intelligence is.

Intelligence is required to understand that is clueless nonsense.

Re: How An AI math breakthrough ignited a controversy

#242

Post by jibal » Thu, Sep 10, 2026, 12:47 AM UTC

vbezhenar wrote: post #14

jibal wrote: post #4

> OpenAI, meanwhile, says its experience with Navier-Stokes could open the door to solving puzzles with more practical relevance. “We are now able to spend millions of dollars on a problem that we really care about and that really matters: developing new materials, finding cures to diseases,” Bubeck said. “All of those things that we have been talking about for a long time—now they seem to be at our fingertips.” Eh?…

He may be hinting that solving these complex mathematical problems will boost OpenAI clients' confidence and encourage them to spend millions of dollars on solving other complex problems.

IOW is just marketing. My point stands.

Re: How An AI math breakthrough ignited a controversy

#243

Post by dekhn » Thu, Sep 10, 2026, 1:41 AM UTC

prmph wrote: post #238

ctenb wrote: post #161

Earlier quoted context omitted.

They didn't write a traditional proof, but a lean program, which can be used to validate proofs formally, using a computer. It's still up to humans to check wether the formalization is sensible, but the proof is correct.

Has Lean itself been proved?

I think pretty much every major mathematician has accepted that the ideas and implementation behind lean is solid.