Jtdylktuy

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:

1. Are there limitations on the kinds of proofs that Coq can verify?




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




3. Do math journals use Coq?




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

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



2. 
   

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

   
   



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



4. 
   

   "How do I go about it if I want to verify a proof using Coq?" The honest answer?

   
   
   
   
   
   1. Take a course on Coq from a computer science department.
   
   
   2. Contact some people who know how to use Coq for formalization of mathematics.
   
   
   3. If unlucky, spend some years formalizing your branch of mathematics.
   
   
   4. Prove your theorem.
   
   
   
   

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.