Lambda the Ultimate

good introductions to the subject of using Proof Assistants in Formalizing 100 Math Theorems

The subject is much broader than formalizing any particular 100 theorems. The articles are about the idea that mathematical proofs should be written in formal proof languages rather than English prose.
This is summarized in Harrison's article:

To be more concrete, our own hopes for formalization are focused on two specific goals:
• Supplementing, or even partly replacing, the process of peer review for mainstream mathematical papers with an objective and mechanizable criterion for the correctness of proofs.
• Extending rigorous proof from pure mathematics to the verification of computer systems (programs, hardware systems, protocols, etc.), a process that presently relies largely on testing.

The first and third articles were two of the most enjoyable things I've read a long time. The second looks interesting; I've not taken a look at the proof of the Four Color Theorem. And the fourth looks useful.

I almost entirely agree with the overall manifesto. I've always had a bit of a penchant for formalism. At one point I had bought into the kool-aid that ZF set theory + the Axiom of Choice was the basis of all mathematics. I started doubting this in college when I discovered, by quizzing a number of my math profs, none knew any of the ZF set axioms or their significance. They only knew the Axiom of Choice and knew of the independence theorems.

But I've also come to realize my formalistic tendancies come at a price. Too much formalism can be a real detriment to actually communicating idea. On the other hand, being overly informal can lead to muddy thinking and an unclear presentation.

The best presentations judiciously combine the best of both worlds, using an appropriate amount of formalism when necessary, surrounded by an insightful and mostly informal explanation of why things are so.

I realize now that most of the proofs that I wrote as an undergrad were much too formal, My proofs were longer than everybody else's and they took me longer to work up. I didn't understand what it took to "prove" something otherwise.

Now, I would say that "proof" in that context is demonstrating to your professor that you have a good understanding why a theorem is true. Hopefully your professor understands it already, so that should be a guide.

The upside of my overly formal proofs is that the few proofs I have transferred into assistants transferred quite painlessly. I'm not really fluent with any proof assisant, but I have toyed with a few, including Coq, Isabelle, and PVS.

In Coq, I never really made it past natural deduction. It was a bit helpful in trying to understand how to apply Natural Deduction.

I got further with Isabelle, and did a few simple inductive proofs. Isabelle proved almost every one automatically: the most I had to do was suggest a lemma and add it as a simplification rule. It was very impressive, but a little boring. The only interesting bit was the computer proofs were actually a bit simpler than what I had wrote; I hardly felt enlightened by the process.

I wrote one reasonably interesting proof about race conditions in PVS, but I wasn't particularly satisfied that the statement I had proved actually corresponded to what I wanted to prove. Confident, yes. Satisfied, no. That is definitely one of the potential downfalls of proof assistants: depending on the theorem, understanding the formal statement thereof is a majority of the effort.

But enough rambling... which proof assistant offers the best path to developing true competence with proof assistants? I was thinking Isabelle, but now the articles have me sold on HOL Light.

Isabelle is impressive, but it also seems complicated and perhaps too automatic. I can apply logic and type theory to other objects quite effectively, but my mind seizes up about metamathematical statements about logic and types. I really want something that might ease some of my mental hangups instead of confirming theorems that I already understand.

I remember I was a huge advocate of a particularly simple programming language for your first language; though I haven't thought in such terms for years. So HOL Light it is.

I was also impressed by the HOL Light tutorial when it comes to storing theorems for later use. HOL Light cannot do that itself. John Harrison suggests using whatever application checkpointing solution you prefer.

My initial reaction was one of revulsion, worried about some complicated and possibly buggy external dependency to cause problems and headaches; but now I see it as a good thing. I discovered they are very easy to use, and in fact, I wish I had known about such functionality before now! Only question I have is, can I get an application checkpointing solution for Mac OS X? I'm not finding any that explicitly advertise support for it.

I think John Harrison is absolutely right in his approach: the big advantage is that it makes the proof kernel simpler and easier to understand. The only real drawback that I see is that this means you can't use two different sets of precompiled proofs. Maybe this could be remedied in some way without giving up external checkpointing, I don't know.

Isabelle is impressive, but it also seems complicated and perhaps too automatic. I can apply logic and type theory to other objects quite effectively, but my mind seizes up about metamathematical statements about logic and types.

Most people when they mention Isabelle really mean Isabelle/HOL. However, Isabelle supports other object logics as well, in particular ZF set theory. I believe Isabelle/ZF is the most natural choice for mathematicians who want to play with formal proofs. Even though they may not know too much about the axioms (that is the case for me too) the standard language of mathematics is that of set theory. Learning to express your thoughts in a different foundation is a serious obstacle.
Also important is the ability to create readable presentations of proofs. Not much about it was mentioned in the articles - there were some pictures that showed the source of HOL Light and Mizar proofs. It is a bit like showing LaTeX markup as an example of how mathematical paper looks like. The presentation abilities of Isabelle are the best among proof assistants today and the simplicity of the Isar proof language allows to roll your own parser and presentation software that is even better.

I liked the proof of the four color theorem, but I wondered about the formalization of it. I would expect some argument on an inductive definition of planar maps (maybe even with some generator function). The proof seems to be very indirect. It made me wonder if there is a better formalization.

(There are several places in the article where by using a reduction some parts of the proofs become trivial, which makes me wonder if those reductions are really necessary.)

Is there a (minimal) set of axioms describing planar graphs?

[The fact that he needed a formalization of real numbers for a combinatorial argument I personally find very strange.]

[I wondered if there is a generator function for describing (abstractly) finite planar graphs, so it would be possible to reduce it to an inductive argument. Though I assume this is not very likely.]

... with his 94^th opinion. On this count, I rather strongly disagree with Dr. Zeilberger, but he's usually entertaining to read anyway.

He might be right that, at this point in time, that spending much time on formal proof is a suboptimal use of both the computer and human time in the pursuit of pure mathematics, but:

1. More formal proof is preferable to less formal proof, despite whatever his opinion might be.

2. Unlike some of his statements that appear to be to the contrary, I don't think formal proof will ever be fully automated, although the goal should be to automate as much as possible.

3. Right now the major interest is in reducing the cost of formal proof substantially, which would make it much more attractive in the future, not to mention have immense benefits.

4. Nicely structured, fully formal proofs can occasionally offer interesting new insights into some aspect of mathematics. Often this insight involves coming up with new decision procedures to automate certain aspects of any given proof.

5. It seems a bit silly, and rather arrogant, to suggest what somebody like Thomas Hale should be doing with his time. I don't think that Dr. Hale is really interested in formalizing Kepler due to his (modest to non-existant) detractors, rather my perception is that he's interested in it for its own sake.