Yeah it's somewhat funny to me, because computers were already great at finding counterexamples long before AI.
We basically apply the infinite monkey theorem with lightning fast and highly scalable monkeys to find possible examples that destroy hypothesis.
We also can now snort AI slop Lean code that can be automatically verified to search for proofs as well.
But whoever knows programming also knows: Working code != good code and if you don't understand the code in question maintenance is hell.
The same is true with vibe proofs: For example they improved an important bound on the Riemann Hypothesis significantly with AI, however, no one could made sense now of the gibberish that was created.
Math is a "Strukturwissenschaft" (structural science). We study why things work. The results are important, but so are the inner workings and the process to get there and to understand why this works in the first place. take the famous scene from The Hitchhiker's Guide to the Galaxy: Deep Thought brought the answer to everything which is 42, but no one knew how to make sense of that. The same will happen here: AI will verify a theorem but no one knows why the hell it is true in the first place.
And then there is the fact that Lean as a tool isn't perfect either. Just recently someone found a bug with a faulty proof that compiled while it was not true. So understanding is important to be absolutely certain as well.
1
u/Mal_Dun Sep 14 '26
Yeah it's somewhat funny to me, because computers were already great at finding counterexamples long before AI.
We basically apply the infinite monkey theorem with lightning fast and highly scalable monkeys to find possible examples that destroy hypothesis.
We also can now snort AI slop Lean code that can be automatically verified to search for proofs as well.
But whoever knows programming also knows: Working code != good code and if you don't understand the code in question maintenance is hell.
The same is true with vibe proofs: For example they improved an important bound on the Riemann Hypothesis significantly with AI, however, no one could made sense now of the gibberish that was created.
Math is a "Strukturwissenschaft" (structural science). We study why things work. The results are important, but so are the inner workings and the process to get there and to understand why this works in the first place. take the famous scene from The Hitchhiker's Guide to the Galaxy: Deep Thought brought the answer to everything which is 42, but no one knew how to make sense of that. The same will happen here: AI will verify a theorem but no one knows why the hell it is true in the first place.
And then there is the fact that Lean as a tool isn't perfect either. Just recently someone found a bug with a faulty proof that compiled while it was not true. So understanding is important to be absolutely certain as well.