> 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.