Comment by Thorentis
8 hours ago
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.
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.
> 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.
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.