Are there examples of originally widely accepted proofs that were later discovered to be wrong by attempting to formalize them using a proof assistant (e.g. Coq, Agda, Lean, Isabelle, HOL, Metamath, Mizar)?
[Math] Proofs shown to be wrong after formalization with proof assistant
formalizationproof-assistantssoft-question
Related Solutions
Although your question is vague in certain ways, one robust answer to it is provided by the subject known as Reverse Mathematics. The nature of this answer is different from what you had suggested or solicited, in that it is not based on any observed data of mathematical practice, but rather is based on the provable logical relations among the classical theorems of mathematics. Thus, it is a mathematical answer, rather than an engineering answer.
The project of Reverse Mathematics is to reverse the usual process of mathematics, by proving the axioms from the theorems, rather than the theorems from the axioms. Thus, one comes to know exactly which axioms are required for which theorems. These reversals have now been carried out for an enormous number of the classical theorems of mathematics, and a rich subject is developing. (Harvey Friedman and Steve Simpson among others are prominent researchers in this area.)
The main, perhaps surprising conclusion of the project of Reverse Mathematics is that it turns out that almost every theorem of classical mathematics is provably equivalent, over a very weak base theory, to one of five possibilities. That is, most of the theorems of classical mathematics turn out to be equivalent to each other in five large equivalence classes.
For example,
Provable in and equivalent to the theory RCA0 (and each other) are: basic properties of the natural/rational numbers, the Baire Cateogory theorem, the Intermediate Value theorem, the Banach-Steinhaus theorem, the existence of the algebraic closure of a countable field, etc. etc. etc.
Equivalent to WKL0 (and each other) are the Heine Borel theorem, the Brouer fixed-point theorem, the Hahn-Banach theorem, the Jordan curve theorem, the uniqueness of algebraic closures, etc. , etc. etc.
Equivalent to ACA0 (and each other) are the Bolzano-Weierstraus theorem, Ascoli's theorem, sequential completeness of the reals, existence of transcendental basis for countable fields, Konig's lemma, etc., etc.
Equivalent to ATR0 (and each other) are the comparability of countable well orderings, Ulm's theorem, Lusin's separation theorem, Determinacy for open sets, etc.
Equivalent to Π11 comprehension (and each other) are the Cantor-Bendixion theorem and the theorem that every Abelian group is the direct sum of a divisible group and a reduced group, etc.
The naturality and canonical nature of these five axiom systems is proved by the fact that they are equivalent to so many different classical theorems of mathematics. At the same time, these results prove that those theorems themselves are natural and essential in the sense of the title of your question.
The overall lesson of Reverse mathematics is the fact that there are not actually so many different theorems, in a strictly logical sense, since these theorems all turn out to be logically equivalent to each other in those five categories. In this sense, there are essentially only five theorems, and these are all essential. But their essential nature is mutable, in the sense that any of them could be replaced by any other within the same class.
I take this as a robust answer to the question that you asked (and perhaps it fulfills your remark that you thought ideally the answer would come from proof theory). The essential nature of those five classes of theorems is not proved by looking at their citation statistics in the google page-rank style, however, but by considering their logical structure and the fact that they are logically equivalent to each other over a very weak base theory.
Finally, let me say that of course, the Reverse Mathematicians have by now discovered various exceptions to the five classes, and it is now no longer fully true to say that ALL of the known reversals fit so neatly into those categories. The exceptional theorems are often very interesting cases which do not fit into the otherwise canonical categories.
The Busemann-Petty problem (posed in 1956) has an interesting history. It asks the following question: if $K$ and $L$ are two origin-symmetric convex bodies in $\mathbb{R}^n$ such that the volume of each central hyperplane section of $K$ is less than the volume of the corresponding section of $L$: $$\operatorname{Vol}_{n-1}(K\cap \xi^\perp)\le \operatorname{Vol}_{n-1}(L\cap \xi^\perp)\qquad\text{for all } \xi\in S^{n-1},$$ does it follow that the volume of $K$ is less than the volume of $L$: $\operatorname{Vol}_n(K)\le \operatorname{Vol}_n(L)?$
Many mathematician's gut reaction to the question is that the answer must be yes and Minkowski's uniqueness theorem provides some mathematical justification for such a belief---Minkwoski's uniqueness theorem implies that an origin-symmetric star body in $\mathbb{R}^n$ is completely determined by the volumes of its central hyperplane sections, so these volumes of central hyperplane sections do contain a vast amount of information about the bodies. It was widely believed that the answer to the Busemann-Problem must be true, even though it was still a largely unopened conjecture.
Nevertheless, in 1975 everyone was caught off-guard when Larman and Rogers produced a counter-example showing that the assertion is false in $n \ge 12$ dimensions. Their counter-example was quite complicated, but in 1986, Keith Ball proved that the maximum hyperplane section of the unit cube is $\sqrt{2}$ regardless of the dimension, and a consequence of this is that the centered unit cube and a centered ball of suitable radius provide a counter-example when $n \ge 10$. Some time later Giannopoulos and Bourgain (independently) gave counter-examples for $n\ge 7$, and then Papadimitrakis and Gardner (independently) gave counter-examples for $n=5,6$.
By 1992 only the three and four dimensional cases of the Busemann-Petty problem remained unsolved, since the problem is trivially true in two dimensions and by that point counter-examples had been found for all $n\ge 5$. Around this time theory had been developed connecting the problem with the notion of an "intersection body". Lutwak proved that if the body with smaller sections is an intersection body then the conclusion of the Busemann-Petty problem follows. Later work by Grinberg, Rivin, Gardner, and Zhang strengthened the connection and established that the Busemann-Petty problem has an affirmative answer in $\mathbb{R}^n$ iff every origin-symmetric convex body in $\mathbb{R}^n$ is an intersection body. But the question of whether a body is an intersection body is closely related to the positivity of the inverse spherical Radon transform. In 1994, Richard Gardner used geometric methods to invert the spherical Radon transform in three dimensions in such a way to prove that the problem has an affirmative answer in three dimensions (which was surprising since all of the results up to that point had been negative). Then in 1994, Gaoyong Zhang published a paper (in the Annals of Mathematics) which claimed to prove that the unit cube in $\mathbb{R}^4$ is not an intersection body and as a consequence that the problem has a negative answer in $n=4$.
For three years everyone believed the problem had been solved, but in 1997 Alexander Koldobsky (who was working on completely different problems) provided a new Fourier analytic approach to convex bodies and in particular established a very convenient Fourier analytic characterization of intersection bodies. Using his new characterization he showed that the unit cube in $\mathbb{R}^4$ is an intersection body, contradicting Zhang's earlier claim. It turned out that Zhang's paper was incorrect and this re-opened the Busemann-Petty problem again.
After learning that Koldobsky's results contradicted his claims, Zhang quickly proved that in fact every origin-symmetric convex body in $\mathbb{R}^4$ is an intersection body and hence that the Busemann-Petty problem has an affirmative answer in $\mathbb{R}^4$---the opposite of what he had previously claimed. This later paper was also published in the Annals, and so Zhang may be perhaps the only person to have published in such a prestigious journal both that $P$ and that $\neg P$!
Best Answer
Since this question was asked in January there have been some developments. I would like to argue that the scenario raised in the question has now actually happened. Indeed, Sébastien Gouëzel, when formalising Vladimir Shchur's work on bounds for the Morse Lemma for Gromov-hyperbolic spaces, found an actual inequality which was transposed at some point causing the proof (which had been published in 2013 in J. Funct. Anal., a good journal) to collapse. Gouëzel then worked with Shchur to find a new and correct (and in places far more complex) argument, which they wrote up as a joint paper.
http://www.math.sciences.univ-nantes.fr/~gouezel/articles/morse_lemma.pdf
The details are in the introduction. Anyone who reads it will see that this is not a "mistake" in the literature in the weak sense defined by Manuel Eberl's very clear answer -- this was an actual error which was discovered because of a formalization process.