alt Hacker News> This new OpenAI result is thus less a mathematical breakthrough and more an oddity of computer scientists being bad at formalizing their design specifications.
Related, another article about proofs that may depend on bad formalizations:
https://news.ycombinator.com/item?id=49994145 - Navier-Stokes Lost in Translation (5 days ago, 237 comments)
AI seems to be very good at getting answers, but not always answers to the correct questions. These remind me of Deep Thought from The Hitchhiker's Guide to the Galaxy, where they got an answer to the ultimate question before actually knowing what the ultimate question is.
> 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.