alt Hacker News>That's not what you'd expect from a serious preprint claiming to solve a problem.
...
>It seems to me, that the AI tech companies would like us to conform to their standards, rather than spend the time and energy to conform to ours.
The entire argument is ugly and unfamiliar methods are used, and nobody's got time to drop everything and understand all that, meanwhile OpenAI didn't even ask us about this, therefore we should reject the paper as "unreadable" and you should be "very angry at OpenAI" today.
No, it's the press where you need to direct your anger. That is the nature of the beast. And being arrogant at the time of mass-disruption is a great way to lose control of everything. Maybe Sam should be sending the bottle of whisky to you.
I think the problem is that they mixed problems that some solutions in Lean (and I consider they solved, assuming someone checked the formalization of the statement) with some solution in English.
I expect most of the solutions in English to be correct or mostly correct, but we all have made and read mistakes mixed with the bla bla bla. In the Mythbuster scale I'd classify them as "plausible" instead of "confirmed".