So i recently learnt that there is now a certain software called ''Coq'' by which one can check the validity of mathematical proofs. My questions are:
Are there limitations on the kinds of proofs that Coq can verify?
How long on average does Coq take to verify a proof?
Do math journals use Coq?
How do I go about it if I want to verify a proof using Coq?
Coq is a proof assistant, and not the only one. Other popular ones are Agda, Isabelle and the related HOL light. They all use type theory as a mathematical foundation (as opposed to first-order logic and set theory), although there is a version of Isabelle that builds ZFC on top of its type theory. And I should mention the venerable Mizar system, which is based on set-theory but it is organized in Bourbaki-style structuralism (I hope I am not misrepresenting Mizar too badly, as I never used it).
Many of these tools were developed by theoretical computer scientists, often for the purpose of verifying proofs of correctness of software. This explains why there is such an emphasis on type theory, but also quite independently of any applications, type theory seems to also be well-suited for organization of mathematics.
Anyhow, the point is that in order to use Coq, you have to learn a new language which sits somewhere between a logic and a programming language. This is not such a small up-front investment. Once you know a bit about Coq, you will discover that there exists a sizable collection of formalized mathematics, which however is minuscule compared to the entire body of mathematical knowledge. Chances are, that your particular topic of interest has not been formalized yet. This presents a problem because a typical working mathematician relies on a large amount of pre-existing knowledge. In fact, a typical mathematician never digs all the way down to the foundations of mathematics, and so is at a loss when presented with the task of building up from scratch their own branch of mathematics. Organization of mathematics is a serious problem, akin to software engineering, and is essentially unsolved.
Let me also answer your specific questions:
"Are there limitations on the kinds of proofs that Coq can verify?" No, not anything you would notice, unless you are a logician or set theorist who makes proofs that are sensitive to the details of the underlying foundations. Coq by default is intuitionistic, but it's easy enough to just add excluded middle and the axiom of choice to it. And you get a lot of universes to play with, in case you want very large collections of objects.
"How long on average does Coq take to verify a proof?" That depends a little bit on what you are doing, but is somewhere between instantaneous and several seconds. Anything longer than that gets people nervous and they start optimizing the proof script. In a larger development long verification times can become a problem. There are a number of techniques to speed up verification, but they rarely have anything to do with mathematics. They're about the internals of Coq and how it goes about checking proofs.
[Note: I originally misunderstood the question as asking how long it takes humans to develop Coq proofs. Here is the original answer.] That depends on how complicated the proof is and how well-versed the user is. Coq is an assistant, which means that a human user directs the proof by breaking it up into chunks that Coq can do by itself. The better you are at directing Coq, the more helpful it will be. A novice will struggle with something like $x + (y + 0) = y + x$ because they will not know which library to use. On the other side of the spectrum is large-scale formalization by teams of experts. I recommend reading the report on the six-year effort to formalize the Odd order theorem, and on the formal proof of the Kepler conjecture, which was another large formalization effort.
"Do math journals use Coq?" Not to my knowledge, except for Formalized mathmatics. However, some conferences in theoretical computer science, e.g. POPL accept formalized proofs as supplementary material.
"How do I go about it if I want to verify a proof using Coq?" The honest answer?
It's sad but true that formalized mathematics is not ready for the mainstream mathematician, and the mainstream mathematician is not ready for formalized mathematics.
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.
