> AI seems to be very good at getting answers, but not always answers to the correct questions.

I don't think that's an accurate summary of the article you linked. The Lean proof solved the exact problem it was supposed to, it just had minor discrepancies from the writeup of the proof (on the level of saying a theorem requires m+4 derivatives when it actually requires m+5 derivatives). Obviously a problem but not really a bombshell.