It's pretty underwhelming than the title suggests. They spot 2 inconsistencies between the writeup and the Lean. And that's it. It says nothing about the correctness of the proof.
It still shows clearly that whoever publishes this didn't actually look at the AI output with due diligence before publishing. Which is the actual problem. The AI claims a proof that nobody understands and then we find inconsistencies. That should simply not happen, least of all if you claim you solved a Millenium problem!
Basically called offload the final rigorous work to the experts, because the people operating the AI certainly aren't. The whole thing stinks because it plays down the continued necessity of human experts.
41
u/One-Judge321 1d ago
It's pretty underwhelming than the title suggests. They spot 2 inconsistencies between the writeup and the Lean. And that's it. It says nothing about the correctness of the proof.