alt Hacker News> Having a Lean proof is an assurance that you proved something. But without going through the definitions, we can't know what you proved.
Sure, even a Lean proof can be wrong. But you made it sound like that because there's a Lean proof, the claims are more likely to be wrong:
>>> Given the constraint (3.5 hours of model effort) having a Lean proof is actually a sign that some of the results are likely weak
Yes for a fixed amount of effort the more you dedicate to formalization the less room there is for exploration. So the constraint is the total budget. The other constraint is if your language doesn't have the concept of gravity it is less likely you are developing the theory of gravity. So if you want to talk about modularity lifting in Lean you need to build up theories on elliptic curves, modular forms, modular curves etc first, because the library doesn't have them even if you consider them elementary. So now if you have a Lean proof with little effort I can infer that it is unlikely to say anything deep about these subjects. If you only have a paper proof, otoh, that doesn't bound your distance from the basics for me.