Comment by Tainnor

I find his scepticism about proof assistants like Lean a bit weird. Of course, there is never absolute certainty, but there are degrees. A proof in Lean is a quite strong guarantee, you'd basically have to have a bug in Lean's core for it to be wrong, which is possible but less likely than a flaw in a proof that hasn't seen much scrutiny because it's rather unimportant (of course, "big" results get so much scrutiny that it's also very unlikely that they were wrong).