I remember reading somewhere that it takes about a week to convert a page of math into something a proof-assistant like Isabelle or HOL Light would accept.

Is this type of conversion something that requires a lot of search and creativity, or is it near-mechanical?

  • 5
    $\begingroup$ I am not sure that this question has a well-defined answer. However, in my view, it often requires creativity to formulate mathematical statements with the degree of clarity needed in different contexts. $\endgroup$ – Geoff Robinson May 15 '14 at 11:08
  • 16
    $\begingroup$ In his paper about the formalization of the prime number theorem, Avigad reported that once he was up to speed it took about a day to formalize a page of mathematics in Isabelle. I recommend that paper for its discussion of the formalization process. repository.cmu.edu/philosophy/31 $\endgroup$ – Carl Mummert May 15 '14 at 12:25
  • $\begingroup$ @Carl Mummert: thanks for that reference, I was not aware of it before and it is extremely useful. $\endgroup$ – Neil Strickland May 15 '14 at 13:27
  • $\begingroup$ I'm making this CW because it seems a bit "discussion-y". $\endgroup$ – Todd Trimble May 15 '14 at 23:35

Formalisation time per page is far from constant. It depends on the material. Sometimes you race through the pages, and at other times you make no progress at all.

Obstacles to formalisation include

  • gaps or errors in the presentation;
  • flights into metamathematical arguments, appeals to global symmetries, etc.;
  • unexpected references to major theorems in some other domain of mathematics.

Sometimes, the author just gives up. Kunen's excellent text Set Theory contains a fine exposition of the development of constructible sets and the axiom V=L, but his proof that GCH follows from V=L is the briefest sketch, a mere 10 lines. This for a proof that took Gödel two years and arguably triggered a mental breakdown. In other cases, you will find that the hardest part of the proof has been left as an exercise.

You need to study your material carefully to see whether it can be formalised with a reasonable effort.

  • $\begingroup$ For a top voted, accepted answer, you've done a very creative job at not answering the question :-) $\endgroup$ – Joe Corneli Dec 5 '17 at 10:16

I'm not an expert (I've played around with HOL a few times, but never fully formalized an interesting theorem), but my experience was that it's similar to writing up a technical proof after you've worked out in your head how to do it: most of the process is pretty directed and you're just filling in details, but you often have to pause at the start of a step to think about the best approach (which requires a small amount of creativity), and every so often you encounter a serious difficulty that requires real thought and creativity to get through (on the scale of patching a small hole in the proof you mostly know, not on the scale of coming up with a new proof in the first place).

  • $\begingroup$ This is the reason why most formalizers have some sort of Automation (Tactics, Solvers, etc.), to make the "mechanical" parts easier. $\endgroup$ – Christoph-Simon Senjak May 17 '14 at 1:32

This may depend sensitively on the subject area. My impression (or perhaps my prejudice) is that proofs in certain areas, like geometric topology, are much farther from being formalized than proofs in most other areas of mathematics.

  • $\begingroup$ I agree with you, but it is worth mentioning that sometimes there are (creative) ways around these difficulties. The formalization of the four color theorem avoided the Jordan Curve Theorem by rephasing it as a graph theory problem. Also, a few years ago someone would have said the same about homotopy theory as you say about geometric topology. But now it is known that homotopy theory is in some sense "built into" constructive Martin-Löf type theory, making it very amenable to proof assistants. But of course, it requires a huge amount of creativity to rephrase a problem like this. $\endgroup$ – Jason Rute May 15 '14 at 15:07
  • $\begingroup$ Probably one problem is that such provers tend to be optimized for intuitionistic logic (except for Mizar, as far as I know), and in my expeirence, continuous mathematics do a lot more proofs by contradiction. While it is trivial to use them for classical mathematics, you will lose much of the computational content of the proofs, and this is something that drives their development. $\endgroup$ – Christoph-Simon Senjak May 17 '14 at 1:38
  • 1
    $\begingroup$ @Christoph-SimonSenjak, both Isabelle and HOL Light use classical logic (with higher order type theory). Proof by contradiction does not present a problem. I agree that in some proof assistants like Coq, there is a desire to extract computational content. Nonetheless, that is not the only motivating drive. HOL Light has an extensive mathematical library, is used to certify the IEEE floating point arithmetic on Intel's chips, as well as verify Hale's proof of the Kepler conjecture. Similarly, Isabelle has been used for a number of verification projects both industrial and academic. $\endgroup$ – Jason Rute May 20 '14 at 17:33

Like Henry, I am not an expert---although I've played around with formal proof assistants.

First, one has to take into account if the background material is already formalized. This can make a big difference. If it is not already formalized then you may need to select a different proof that is more computational and avoids tricks that venture into other territory. (If the proof you are formalizing is fairly new, you may need to do that work yourself which obviously takes time and creativity.) Alternately, one needs to formalize this background material (which can be satisfying, but also takes time).

Second, it matters if you are going for building a beautiful library of math or just trying to hack together some proof until the computer says "proved". In the former case, you may actually spend a few weeks thinking about how you want to set up the whole structure. (As an example, would you define a ring as an Abelian group with multiplication, or would you define it from scratch? If you define it as an Abelian group, then you could also use all the theorems you proved for Abelian groups for rings as well.)

Last, it takes some time to get into the swing of using a proof assistant, but after that, it is fairly mechanical. Nonetheless, there will be a number of times when you think to yourself "this is obvious, but I guess the computer doesn't know that". Then you have to figure out how to convince the computer that it is true, usually by breaking the proof into some trivial logic. However, as with all things, with experience this happens less and less.

I am sorry I can't give you a rate like "one day per page", mostly from my lack of experience.

  • 2
    $\begingroup$ The issue of background material is very important. In Gonthier's formalization of the four-color theorem, for example, the Jordan Curve Theorem was a major issue. Formalizing the full JCT would have been a major "digression" as it were. It required considerable creativity to figure out how to work around it. See Gonthier's paper for more information. research.microsoft.com/en-us/um/people/gonthier/4colproof.pdf Similarly, when Avigad formalized the prime number theorem, creativity was needed to find the version of the proof that would be the easiest to formalize. $\endgroup$ – Timothy Chow May 15 '14 at 17:19

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.