First of all, this is clearly Lean not Coq (and certainly not “CoQ”). While the distinction is minor, it does cause me to question if you may have fallen victim

First of all, this is clearly Lean not Coq (and certainly not “CoQ”). While the distinction is minor, it does cause me to question if you may have fallen victim to the Dunning–Kruger effect here. Perhaps I’m wrong, but it may be worth some self-evaluating. Furthermore, I think you’re missing the forest for the trees here. My only real claim is that theorem proving and computation are two sides of the same coin. Either way you start with data, apply a sequence of established transforms to that data, and stop when you’ve reached an accept or reject state. The precise encoding of the input, transforms, and accept/reject states is unimportant. That said, we do seem to agree that Euclid’s original formulation is not a “true” proof. As you mentioned, many mathematicians have found cause to go back over the same theorem using more formal methods. While it’s true that for this particular proof-by-intuition no faults have been found, that certainly does not generalize to all proofs by intuition, and as such it’d be far more appropriate to compare a complete traditional proof to the complete computer proof. If you were do do this I suspect you’d find them quite similar, as axiomatic computer proofs tend to use the exact same fundamentals as axiomatic pen and paper proofs. Finally, your claim that theorem provers have never found significant faults in a famous conventionally proved result is shown incorrect by a simple Bing query. See https://www.math.sciences.univ-nantes.fr/~gouezel/articles/morse_lemma.pdf https://www.math.sciences.univ-nantes.fr/~gouezel/articles/m.... While the overall result did hold, formal verification discovered a bone fide hole in the widely accepted, published, peer-reviewed, etc etc etc, paper. Plenty of other examples are available at https://mathoverflow.net/questions/291158/proofs-shown-to-be-wrong-after-formalization-with-proof-assistant https://mathoverflow.net/questions/291158/proofs-shown-to-be.... You also seem to be ignoring the fact that many theorems have only been proven via computational analysis.