> 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.
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.