Comment by xyzsparetimexyz 18 hours ago Yeah but how am I meant to verify that the proof is proving what it says it is? 3 comments xyzsparetimexyz Reply margorczynski 13 hours ago Verify the statement is correct + it doesn't introduce any new axioms + doesn't use "sorry" etc.Order of magnitudes easier than verifying the whole thing by hand and gives a much better guarantee of correctness anthonyrstevens 8 hours ago Do you know what "sorry" means in the context of Lean? xyzsparetimexyz 11 hours ago How am *I* meant to do that
margorczynski 13 hours ago Verify the statement is correct + it doesn't introduce any new axioms + doesn't use "sorry" etc.Order of magnitudes easier than verifying the whole thing by hand and gives a much better guarantee of correctness anthonyrstevens 8 hours ago Do you know what "sorry" means in the context of Lean? xyzsparetimexyz 11 hours ago How am *I* meant to do that
Verify the statement is correct + it doesn't introduce any new axioms + doesn't use "sorry" etc.
Order of magnitudes easier than verifying the whole thing by hand and gives a much better guarantee of correctness
Do you know what "sorry" means in the context of Lean?
How am *I* meant to do that