20
$\begingroup$

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?

Improve this question
$\endgroup$
5
  • 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
    Commented May 15, 2014 at 11:08
  • 18
    $\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
    Commented May 15, 2014 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
    Commented May 15, 2014 at 13:27
  • $\begingroup$ I'm making this CW because it seems a bit "discussion-y". $\endgroup$
    – Todd Trimble
    Commented May 15, 2014 at 23:35
  • 2
    $\begingroup$ The De Bruijn factor is a measure of how much harder it is to write a formal mathematical proof instead of an informal one. $\endgroup$
    – Timothy Chow
    Commented Jun 13 at 15:25

5 Answers 5

Reset to default
21
$\begingroup$

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.

Improve this answer
$\endgroup$
2
  • 8
    $\begingroup$ For a top voted, accepted answer, you've done a very creative job at not answering the question :-) $\endgroup$
    – Joe Corneli
    Commented Dec 5, 2017 at 10:16
  • $\begingroup$ My reaction is the opposite, that it is a very clear answer. $\endgroup$
    – provocateur
    Commented Jun 14 at 2:09
10
$\begingroup$

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

Improve this answer
$\endgroup$
1
  • $\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
    Commented May 17, 2014 at 1:32
6
$\begingroup$

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.

Improve this answer
$\endgroup$
3
  • 1
    $\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
    Commented May 15, 2014 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
    Commented May 17, 2014 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
    Commented May 20, 2014 at 17:33
6
$\begingroup$

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.

Improve this answer
$\endgroup$
2
  • 3
    $\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
    Commented May 15, 2014 at 17:19
  • $\begingroup$ Here's a better link for Gonthier's paper: A computer-checked proof of the Four Color Theorem. $\endgroup$
    – Timothy Chow
    Commented Jun 13 at 15:30
3
$\begingroup$

In a recent interview, Terence Tao opined on this:

When you gave a talk about a different mathematical project, someone asked you if you wanted to formalize it, and you basically said that it takes too long.

I could formalize it, but it would take a month of my time. Right now I think we’re not yet at the point where we routinely formalize everything. You have to pick and choose. You only want to formalize things that actually do something for you, such as teach you to work in Lean, or if other people really care about whether this result is correct or not. But the technology is going to get better. So I think the smarter thing to do in many cases is just to wait until it’s easier. Instead of taking 10 times as long to formalize it, it takes two times as long as the conventional way.

I think he is trying to say that Lean proofs currently take 10 times as long as informal ones.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .