Formal Proof I

Formal Proof – Theory and Practice, by John Harrison

Among the four articles on formal proofs in the Notices this is the one I enjoyed most.

John Harrison is the creator of HOL Light, one of the systems for doing formalized mathematics. He got hired by Intel in 1998 after the famous Pentium bug to work on formal verification of algorithms used in Intel chips (AMD hired David Russinoff). Harrison was one of the first people in Western Europe working in formal verification who noticed the value of Mizar’s declarative formal proof style and the existence of Mizar itself. He is a living example that formalized mathematics is relevant now and you can even earn living doing it if you a lucky genius.

I found some paragraphs of the “theory” part a bit too basic. I think explaining that

for example as we write “x+y” to denote mathematical object “x plus y“, we can use to denote the proposition “p and q“

is not needed for the readers of Notices of American Mathematical Society. This stuff is taught in some high schools.

There two kinds of people doing formalized mathematics: those who like set theory and those who prefer types. Harrison is a types guy (I like sets). I think that the difference is similar to the one between dynamically and statically typed programming languages. You can argue forever on the relative merits of the two approaches. Harrison provides an interesting discussion on this, free of nonsense typical for some types people (see a later post on Hales article).

I liked a lot Harrison analogy between replacing the “social process” that now determines the correctness of (informal) proofs by machine verification and replacing the social process that Greeks used to decide scientific questions by experimental verification.

One thing that I found lacking in the article is a bolder vision of what can be done with the mathematical knowledge encoded in a computer. Harrison presents two hopes for formalization: supplementing or replacing peer review and applications to modeling and verification of computer systems. That is very realistic and down-to-earth, I think too much so. Harrison notices the possibility of presenting the same proof at different levels of details to suit different readers, something Tiddly Formal Math tries to do. That’s good, but at least he should also mention possibility of easy cross-referencing and visualizing graphs of dependencies between theorems and definitions. Metamath Proof Explorer cross references everything and is a great resource if someone wants to check, say, if a given fact depends on the Axiom of Choice. A similar thing done with HyperGraph for example would be really cool. And mathematics needs to be cool.

Advertisement

Tags: formalized mathematics, Notices