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