The AI industry learned to generate. The next leap is learning to prove. A 25-year-old mathematician is betting $1.6 billion on the gap between the two.
This is a good read, much worth thinking about. Here are my immediate thoughts. It is territory well worth covering.
Within any consistent axiomatic system there is ground truth. No such system's consistency can be proved internally, that cannot be part of it's ground truth. There will always be unprovable statements. Not intractable --- fundamentally unprovable. This is a formal ground truth of axiomatic systems of sufficient complexity to include arithmetic.
Formal models are many things: powerful, useful, beautiful and wonderful aids to understanding, generalisation and abstraction. When they are these things and model some experienced or observed aspect of the practical world around us they are simplifications and approximations. That is what makes them all those things. It is also what makes them computationally tractable. An internal ground truth in the model is not a ground truth about the reality which it simplifies and represents.
Logical analysis and verification sit wholly within a formal model of the world --- with all the approximations, simplifications and assumptions built in to the axioms from which it is constructed. They verify the connection from assumption and approximation to conclusion, not some link to underlying truth, whatever that could mean.
This is what changed between modern AI and the old logical cybernetics, which is intractable beyond extremely contained frameworks. Certainly those constraints can and will be pushed back significantly but the stereotypical cold, logical cyborg will remain fictional, this is not how minds can operate in a real world. But such formality is also certainly an important layer in learning and explaining things. And beautiful in its own right.
Mathematics has grown in this regard in many steps. Perhaps Galileo and infinitesimals could be seen as a core break four centuries ago. Incompleteness was another fundamental shift, three centuries later. Then Chaos, but these are just a few highlights.
Really enjoyed the historical sweep, and incompleteness is exactly where the article's claim gets tested.
What Gödel broke was provability. What he left untouched was verification: whether a given derivation is valid stays mechanically decidable. The article's ground truth is only that second thing, which is why it survives the break.
And fully agreed, the compiler certifies derivation, not reality. Math just happens to be the one place where that's enough, because its territory is the derivation itself.
Thanks, I was meaning to find out more about this company. I don’t know Lean well but I always assumed that if it’s like any other programming language, the key is that it is generative. As in, you have primitives and operators and can start just combining them to generate new things. In lean’s case those may become new lemmas or theorems, which are potentially more useful than an LLM just generating a novel. Additionally, like I wrote about in the context of robotics, I’m a big believer in the pairing of language models with tools, so I’m looking forward to seeing what comes of this!
Yes. It’s a uniquely compelling company. You can follow their founder, Carina Hong (@CarinaLHong), and Founding Mathematician Ken Ono (@KenOno691) on X to stay close to how it unfolds.
This is a good read, much worth thinking about. Here are my immediate thoughts. It is territory well worth covering.
Within any consistent axiomatic system there is ground truth. No such system's consistency can be proved internally, that cannot be part of it's ground truth. There will always be unprovable statements. Not intractable --- fundamentally unprovable. This is a formal ground truth of axiomatic systems of sufficient complexity to include arithmetic.
Formal models are many things: powerful, useful, beautiful and wonderful aids to understanding, generalisation and abstraction. When they are these things and model some experienced or observed aspect of the practical world around us they are simplifications and approximations. That is what makes them all those things. It is also what makes them computationally tractable. An internal ground truth in the model is not a ground truth about the reality which it simplifies and represents.
Logical analysis and verification sit wholly within a formal model of the world --- with all the approximations, simplifications and assumptions built in to the axioms from which it is constructed. They verify the connection from assumption and approximation to conclusion, not some link to underlying truth, whatever that could mean.
This is what changed between modern AI and the old logical cybernetics, which is intractable beyond extremely contained frameworks. Certainly those constraints can and will be pushed back significantly but the stereotypical cold, logical cyborg will remain fictional, this is not how minds can operate in a real world. But such formality is also certainly an important layer in learning and explaining things. And beautiful in its own right.
Mathematics has grown in this regard in many steps. Perhaps Galileo and infinitesimals could be seen as a core break four centuries ago. Incompleteness was another fundamental shift, three centuries later. Then Chaos, but these are just a few highlights.
Really enjoyed the historical sweep, and incompleteness is exactly where the article's claim gets tested.
What Gödel broke was provability. What he left untouched was verification: whether a given derivation is valid stays mechanically decidable. The article's ground truth is only that second thing, which is why it survives the break.
And fully agreed, the compiler certifies derivation, not reality. Math just happens to be the one place where that's enough, because its territory is the derivation itself.
Thanks, I was meaning to find out more about this company. I don’t know Lean well but I always assumed that if it’s like any other programming language, the key is that it is generative. As in, you have primitives and operators and can start just combining them to generate new things. In lean’s case those may become new lemmas or theorems, which are potentially more useful than an LLM just generating a novel. Additionally, like I wrote about in the context of robotics, I’m a big believer in the pairing of language models with tools, so I’m looking forward to seeing what comes of this!
Yes. It’s a uniquely compelling company. You can follow their founder, Carina Hong (@CarinaLHong), and Founding Mathematician Ken Ono (@KenOno691) on X to stay close to how it unfolds.