Hacker News Reader

Comment by malisper | Hacker News Reader

> 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

View on HN

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.

Would I be correct in saying that you're making a claim about how difficult the statement is to prove, rather than the accuracy of the proof?

I may be simplifying things a little but it is two-fold: one Lean lets you call your theorem whatever you want, but if your vocabulary doesn't include the math objects I am interested in, it is unlikely that you said something interesting about them; secondly steps are painfully small in formalized math and even then you have to fight to get Lean not confused about what you are doing (like typeclass inference), so what you can do in three and half hours from a low base is quite bounded.

Yes, that is the assertion here.

Reply on news.ycombinator.com