Re:OpenAI withdraws three mathematical results
by Thorentis on Thursday October 08, 2026 @05:09AM
(#50003536)
How do we even know the premises of the "verified" Lean proofs are correct? The more I think about these results, the more I'm convinced this is like a junior engineer who writes 100 unit tests and shares a screenshot of Pytest being all green, but you check the code and most of them are just doing assert True.
[ Parent
| on HN ]
Re:OpenAI withdraws three mathematical results
by hazbot on Thursday October 08, 2026 @05:34AM
(#50003712)
> How do we even know the premises of the "verified" Lean proofs are correct?
We let the experts investigate. If the results are dodgy, then the next batch of results will have to do more upfront work to demonstrate their worth. If there is gold in them hills, then this is exciting though very disruptive for the math community.
Re:OpenAI withdraws three mathematical results
by MisterMunchkin on Thursday October 08, 2026 @05:51AM
(#50003816)
But like with all slop, why should I have to spend my time dealing with your worthless slop? If I wanted slop I could just make it myself.
Re:OpenAI withdraws three mathematical results
by sebzim4500 on Thursday October 08, 2026 @05:30AM
(#50003679)
You read them? People are acting as if Lean definitions are some black art that only 3 people understand, but you can literally just do the tutorial and you will be able to understand the statement of most of these results.
Understanding the proofs is a different story unfortunately.