Comment by sashank_1509

Super-intelligence that’s going to end mathematics as we know it surely must be held to a higher standard than puny humans?

More seriously the problem is the complete utter lack of care OpenAI has shown in their desperation to demoralize mathematicians with their new LLM. In their words, it took 3 hours of ChatGPT pro per result, why not spend a hundred hours per result formalizing it, checking if the formalization matches the natural language proof, and whether the argument could be made more simpler and readable. Any human paper has hundreds of hours of work put into it, but OpenAI who is absolutely adamant in demoralizing the mathematical community and demonstrating their superior “intelligence” will only spend 3 hours, write unreadable, inscrutable proofs, not formalize all of them, and then dump it on the mathematical community for some reason.