Earlier quoted context omitted.
I'm not sure if you meant it this way, but this is more an insult directed at mathematics, not openAI.
That would be an incorrect interpretation
How An AI math breakthrough ignited a controversy
141–150 of 243 posts
Re: How An AI math breakthrough ignited a controversy
#142Re: How An AI math breakthrough ignited a controversy
#143Earlier quoted context omitted.
Its called an analogy
It's one of the seven most important problems in mathematics. Pick a better analogy.
(Not that I think the comparison to pi digits make sense)
Re: How An AI math breakthrough ignited a controversy
#144> “I certainly don't expect the industry to continue to spend millions of dollars to solve problems in mathematics, because there is no profit in it,” Columbia University mathematician Michael Harris wrote in an email to Science. But he worries the highly publicized achievement will be “extremely damaging to mathematics; it convinces decision makers that human mathematicians are obsolete, and it convinces young peopl…
I only have an undergrad in math, so very little understanding, but I'd be pretty surprised if it couldn't do forall just as well. Like, say it found this counterexample which relies on axial stretching or whatever approach. Then it already knows how that made the proof work, and can use it to try to prove NS has smooth solutions modulo this particular kind of defect (so it could make some statement about cohomology,…
I think you cannot assume so, because pattern matching is not reasoning.
Re: How An AI math breakthrough ignited a controversy
#145Earlier quoted context omitted.
Are you asking if it uses additional axioms of `sorry` in the proof? It's easy to check that it doesn't by compiling it and telling lean to list the axioms.
It's highly non-trivial to confirm that the theorems written in Lean are actually the same as the Navier–Stokes (non-)theorem.
This doesn't guarantee that the statement is correct (Lean cannot do that), but makes it highly likely.
Re: How An AI math breakthrough ignited a controversy
#146Regardless of what you think of the priority dispute issue discussed on sibling threads, I’m highly skeptical of the closing quote that this Navier Stokes result means that the same approach of casually spending a few million on agentic computation is going to solve end to end materials design or drug development. Those problems can’t be formally verified with an automated theorem prover. We have a lot of physics bas…
Yeah, I think you can't just throw money randomly at problems and expect results unless you know a line of attack that can get you all the way. OpenAI chose the line of attack only after it became known to them via rumors. They "front-ran" the researchers.
Separate from all the allegations of more nefarious actions and ethical issues, that’s the most charitable version of what happened here.
Re: How An AI math breakthrough ignited a controversy
#147Re: How An AI math breakthrough ignited a controversy
#148> “I certainly don't expect the industry to continue to spend millions of dollars to solve problems in mathematics, because there is no profit in it,” Columbia University mathematician Michael Harris wrote in an email to Science. But he worries the highly publicized achievement will be “extremely damaging to mathematics; it convinces decision makers that human mathematicians are obsolete, and it convinces young peopl…
> it convinces decision makers that human mathematicians are obsolete, and it convinces young people that their passion for mathematics has no future Maybe those things are true, so maybe they should be convinced?
I don't see why mathematicians think they should be an exception here.
Re: How An AI math breakthrough ignited a controversy
#149Regardless of what you think of the priority dispute issue discussed on sibling threads, I’m highly skeptical of the closing quote that this Navier Stokes result means that the same approach of casually spending a few million on agentic computation is going to solve end to end materials design or drug development. Those problems can’t be formally verified with an automated theorem prover. We have a lot of physics bas…
> Those problems can’t be formally verified with an automated theorem prover. It certainly seems like any problem that is amenable to reinforcement learning will be solved.
Re: How An AI math breakthrough ignited a controversy
#150The whole thing reeks of the desperation of an unprofitable venture-backed startup looking for its next PR win to keep the wind in the sails. But I think what’s being overlooked in the race to claim absolute credit is that both sides ultimately relied on a LLM (and one of OpenAI’s at that). Either a human researcher made a breakthrough discovery with the help of Codex, or the latest GPT model made a breakthrough with…