Ok so Claude says that the Riemann hypothesis is proven and gives you 1200 pages of math symbols backing it up. Now what?
You probably say "now a human can verify it" but what if the humans are wrong? What is the source of truth?
You probably say "now a human can verify it" but what if the humans are wrong? What is the source of truth?
The source of truth here is the code we wrote for the formal verification system.
But that's not how it works; rather it tells you about the specific issue with a particular step in the proof, which you then debug, as you would with code that isn't compiling (or not passing some static analysis test).