Comment by UltraSane

What a ridiculous thing to say. If it was verified in Lean we could be much more confident the proof is correct.