alt Hacker NewsHaving a Lean proof is an assurance that you proved something. But without going through the definitions we can't know what you proved. This part can't be mechanized. It's like a program that is compiled will likely run, but you can't say it will produce what you want. FLT stands out as everyone can read the statement. This is not true for most open math problems.
> 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