linkedin.com
È l’Epistemia, bellezza.
A few days ago, the story was everywhere: AI had essentially cracked Navier–Stokes, formal verification was there, and the usual chorus followed.
“Superhuman.”
“Mathematics… | Walter Quattrociocchi
È l’Epistemia, bellezza.
A few days ago, the story was everywhere: AI had essentially cracked Navier–Stokes, formal verification was there, and the usual chorus followed.
“Superhuman.”
“Mathematics is solved.”
“Verification changes everything.”
Not so fast.
A new paper analyzing the case makes a much more interesting point.
Lean may correctly verify the formal object it is given.
But that does not guarantee that the formal object is semantically faithful to the original natural-language proof.
In other words:
the verifier can be perfectly right while the pipeline is epistemically wrong.
This is exactly the point we have been making about current AI systems.
They are extraordinarily powerful heuristic machines.
But their reliability depends on the verifier, on the target, and on whether the verification layer is actually checking the claim we think it is checking.
A perfect verifier attached to the wrong target is not a solution.
It is a very convincing failure mode.
And this is why th
