This is a most excellent place for technology news and articles.
Of course, Open AI isn't going to cite references for all the sources it spudered through to assemble the proof, and likely will be borrowing on a lot of work already done by mathematicians.
So, breaking the rules maintained by all institutions of academic research.
Incidently, LLMs can't logic. We've discovered this when they screw up simple logic problems. They have to depend on human explanations of logical processes, usually when someone else reported on the solution to the logic puzzle.
OpenAI researchers are all dirtbags.
OpenSI*
TLDR:
Most of the "mathematical breakthroughs" from AI have been done by loading all available recent research from humans solving the problem, and then collating it while skipping reviews and telling the humans who did the work it would literally be "too complicated" to explain the AI didn't actually do anything...
It's all just lies to drive up stock prices, what they release appears to be stuff that would be released shortly anyways, it's just being dumped at once 99% of the way done before it's verified.
I don't have an English source, but on this trustworthy French public service radio scientific podcast, 2 mathematicians (from reputed organizations, including one Henri Poincaré Prize) are discussing the Navier-Stokes AI solution. https://www.radiofrance.fr/franceculture/podcasts/la-science-cqfd/ia-et-mathematiques-quand-la-solution-pose-probleme-5497880
They say that the results are legitimate and proven through mathematical proof software. It did build on recent progress by humans, but it would still have taken years for humans to get there, because AI could explore so many paths in a much shorter time than a few human specialists can.
They explain the help from AI is technically remarkable, and people who don't recognize it are in denial. They think mathematics research without AI will not make any sense soon. There's also some hope that it will allow focusing on new interesting problems that the current AI cannot solve yet. They also discuss the problem of AI being owned by foreign mega corporations and that's a risk for public research produced for the common good.
I'm probably going to get downvoted for this unpopular opinion here, just know that I also hate the social and environmental impact of AI, but denying its effectiveness is clearly irrational now.
How the robot proves these statement is by writing LEAN code that represents the math. If the lean compiles, the math was valid. If it doesn't, it tries again.
It will do this forever until it finds a solution.
Goedel predicted this in 1933, btw. From his work on formal systems, he ascertained that since every mathematical statement is trivially true following from the rigorous application of the axioms of mathematics or entirely false, theorems could be checked and proven automatically.
These systems are able to prove statements at a scale beyond humans, because they have effectively infinite time to exhaustively explore applying every rule.
Unfortunately, this isn't all that helpful for the various fields of math as a whole. Effectively they have a list of statements and a second column with 'true' or 'false', but the actual route taken by the models to get that answer is often incredibly indirect and therefore difficult to gain insight from and apply to new areas. The approach taken to produce an answer is often more valuable to the field than the answer itself.
The field moves forward when the people in it understand the new results and techniques sufficiently to begin asking new questions, simply giving the answer isn't all that useful. The robots cannot (yet) do this. Someone has to, at a minimum, pose the question in formal mathematical language. There are an infinite number of true statements in mathematics ( trivial example 1=1, 2=2, ...) asking the interesting questions is the important part. The field will still only advance as fast as the people in it are able to digest results.
Further, results in pure math do not generalize to the more applied fields that directly affect our ability to do things. Most engineering formulae are NOT rigorously true - they are weak approximations with envelopes of applicability. The same is true even in base physics. So while a robot can crank through ten million lines of lean to prove an obscure theorem, it cannot think about physics for a week and come up with a theory of quantum gravity.
Well written and agreed. I think suddenly having many new statements that are proven true, with probably some of them being unexpected, will have serious impact on research directions, even if it still takes time to digest and find useful applications.
I am more skeptical. Even with Navier Stokes, I never heard anyone actually internalize the result and have trust in it. I just heard vague lean-dih waving.
Supposedly it's 26000 subtheorems of goobledigook, feels untameable.
Mathematicians seemingly: Axioms are correct, we trust lean => Result correct.
As a physics, CS thinker: AI probably found a bug in our axioms. And/or usual self-referential math issue. And/or connected to Goedel's incompleteness. Also I wonder why I even trust lean as much, havent even read its code. Most software works great until somebody starts poking at its limits.
Even if it's finding bugs in those, it would be progress. Imagine we can find bugs like that in many other problems, that's pretty valuable. Agreed it will take time to digest proofs and produce something new out of it.
Because the AI contribution was so huge was surely the reason openAI did not want to give any credit to the researches that worked on the foundation for that breakthrough.
My server contribution is huge too, hosting shit all the time. Given as much, I wonder if I can void the licenses of the software I use.
Depends. Are you an AI company?
Assume all that is true, AI can really do well in these fields, but there are some other fields it can't do well in.
Now who is going to work on those fields? Who is going to take the risk of studying for it, practicing for years, being an expert in the field that takes maybe a decade, and the AI can suddenly solve your field too, and you don't get anything.
Yeah, we also need to solve the attribution and retribution for the people who contributed to the result, and we can't expect this to happen from mega corps alone.
Ok but actual practical real world use case exists for this? So we know that in theory an imaginary thing that doesn't exist could create a singularity event?
Honestly seems like it's not useful but I'm not a mathematician so I don't really know.
I think many theoritical researchers do not care about practical applications (from physics university time, I even remember a disdain from some students about applications because it's "dirty", meaning badly approximated).
In any case, it's hard to predict, but sometimes theoritical results have real world impact eventually. Crazy theories like quantum physics and Relativity are used to for computing (semiconductors and newer quantum computers) and GPS now.
Having this proven solution will probably motivate new research directions, and it could improve the understanding of this fluid mechanics equations, which has applications everywhere fluids are used...
Doing 10%, or less, of the work and taking credit for it. Add this to the bucket for "Reasons AI can replace the C-suite"
It's a 20/80 rule thing.
Coming up with a proof is the first 20% of work. Actually checking and validating the proof is the next 80% of work.
I learned it as 80/20 rule where the first 80% of progress is made with 20% of effort, and the last 20% of progress takes 80% of the effort.
It's true im many layers deep in it help
Yeah same idea. Another good one along the same lines is
“We didn’t do this because it’s easy. We did it because we thought it would be easy”
I'm assuming this is about the 372 math "breakthroughs" they recently posted. The top "discoveries" seem to be trivial cases that don't give much insight into the broader conjectures and many of them don't even have a lean proof so they can't remotely be trusted as correct (and having a lean proof isn't necessarily proof that it's correct either). They basically crapped out everything the AI did and said you figure out!
If you skip peer review I don't give a shit about what you "publish."
I'm not vetting your bullshit when I write.
Several employees within OpenAI believe their technology has rendered math dead anyway, according to people who have spoken with them.
They do believe a lot of things about their magic word machine.
Reminds me of the Mechanicus in 40k. “We just worship the machine and it does what we want it to. How does it work? No one knows!”
they trying to live vicariously through other more successful people in that subject, by projecitng.
ChatGPT, prove to me that Sam Altman is an idiot.
prove to me that Sam Altman is an idiot.
I actually did this and it returned 8 pages of examples.
It should be basic babymath with him and that stressed face.
Compared to what OpenAI is claiming its word machine has solved (without any human verification for the claims so far, not even in OAI), the scribbles kinda are (just highschool math).
Now, after release, here's an example of the initial thoughts of someone who had spent time on one of the solved problems:
I think people really need to understand the "it just took a bunch of public work and connected the pieces" isn't a gotcha for LLMs: it's one of the sales pitches. The cross-discipline general knowledge combined with the ability to churn huge datasets to find connections across already-known work, and extrapolate to or derive novel findings, is exactly one mode of superhuman success that AI companies have been trying to achieve.
The bigger issue is that they may be camping human efforts then kill-stealing the last hit on the boss by burning millions of dollars to get a proof a few days/weeks/months earlier than when it would have happened without AI. Basically, waiting for problems to be all-but-formally solved, then beating the researchers to the punch; like the recent Millenium controversy
In other words, this person doesn't yet know if it's correct.
Hinestly, AI can be a great tool to further evolve mathematics,but you still have to understand every gory detail it did to solve the problem. If you can't do that, it's not solved.
Also all ML models have some accuracy less than 100%, that means you can’t trust it. The whole point in the proof is perfection
What if it does some wrong or fake equations ? Like who cares? USA is putting AI first, not mathematicians.
If you can't follow the logic of the steps of the proof, it's not a proof.
Granted, you may not be skilled in logic, but some of us, mathematicians, specifically, are.
If no mathematician can follow the logic, it's not a proof.
