10 ms·
It may be for this theorem there's a succinct description, but still needs to be checked carefully. However, there are others that are non-trivial.
by rencrisa 2mo ago
It may be for this theorem there's a succinct description, but still needs to be checked carefully. However, there are others that are non-trivial.
- nilkn 2mo agoIn some cases you're right, but I think that's often a symptom of mathematics in Lean being relatively immature (i.e., it will get much easier with time). Even then, verifying the statement in Lean is correct is still much easier than verifying the natural language proof is correct.