> I think that's a bit too harsh. An entire complicated proof concocted solely looking at a computer screen in Coq? Nobody is suggesting this, and in this case

> I think that's a bit too harsh. An entire complicated proof concocted solely looking at a computer screen in Coq? Nobody is suggesting this, and in this case, it was indeed "ported" to Coq from existing sketches. The distinction here isn't between on-paper-first vs computer-first. The distinction here is between using a custom computer program to perform computations for a mostly-paper proof, versus taking an existing general-purpose theorem-checker (Coq, in this case) and writing down the entire proof in its language so it can check it.