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.
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.