In my answer I am referring to other systems like **HOL Light**, but if the formal verification mentioned below, would be implemented in **Coq** the situation would not be much different.

**Do math journals use Coq?**

No, they do not, but there is one exceptional example that needs to be remembered and I will mention it below. Usually, formal verification is applied to results that have previously been checked by humans. However, there is one amazing result that the only way we can be sure it is true is because it was formally verified. I am quoting after Wikipedia:

*In 1998 Thomas Hales, following an approach suggested by Fejes Tóth (1953), announced that he had a proof of the Kepler conjecture. Hales' proof is a proof by exhaustion involving the checking of many individual cases using complex computer calculations. Referees said that they were "99% certain" of the correctness of Hales' proof, and the Kepler conjecture was accepted as a theorem. In 2014, the Flyspeck project team, headed by Hales, announced the completion of a formal proof of the Kepler conjecture using a combination of the Isabelle and HOL Light proof assistants. In 2017, the formal proof was accepted by the journal Forum of Mathematics, Pi.*

The original proof of the Kepler conjecture was submitted to Annals of Mathematics and the panel consisted of 12 referees! It was published after a very long referee process. The reason why the referees could not check correctness of the proof was because it involved computer code for the verification of thousands of cases. This was the reason why Hales decided to write a formal proof that was verified by a computer. Note that all numerical computations have also been verified formally. This was possible because he was using the interval arithmetic that allowed for a rigorous estimates of the approximation.

**How long on average does Coq take to verify a proof?**

One may expect that while a proof was written by humans who are rather slow, a computer should be able to check it quickly. Not necessarily. Regarding the formal proof of the Kepler conjecture the time needed for a formal verification was astonishing. Here is a quote from https://code.google.com/archive/p/flyspeck/wikis/AnnouncingCompletion.wiki:

*The term* the_nonlinear_inequalities *is defined as a conjunction of several hundred nonlinear inequalities. The domains of these inequalities have been partitioned to create more than 23,000 inequalities. The verification of all nonlinear inequalities in HOL Light on the Microsoft Azure cloud took approximately 5000 processor-hours.*

The verification was in HOP Light, but I would not expect that in Coq verification would be much faster.