“There’s a perception of mobster behavior” from leading AI companies, one mathematician tells WIRED as OpenAI prepares to release more than 100 new solutions to unsolved problems.
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.
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…
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.
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.
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.
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…
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.