Hacker News Reader

Yeah but how am I meant to verify that the proof is proving what it says it is?

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

How am *I* meant to do that

Do you know what "sorry" means in the context of Lean?