Vdash, monotone and ikiwiki

A lot of new stuff appeared yesterday on the Vdash home page. There is a very nice collection of links to information about formalized mathematics. The most interesting however is the roadmap page which states that Vdash will be based on ikiwiki wiki compiler and the monotone version control system. This represents a major shift in the concept.

Formal Proof II

Imagine that a programming guru is asked by a person who wants to learn programming how to start. The guru tells the novice that he should get some nice Linux distribution like Gentoo that has all he needs – vi and gcc. He also shows the novice some Linux kernel code to demonstrate the wonderful things someone with knowledge of programming can do. The n00b is immediately enlightened. Or, more likely, runs away in horror.

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.

Formalized Mathematics in the Notices of the AMS

I remember in 2004 when I was trying to find a formalized mathematics project to contribute to I did a search on formalized mathematics in AMS Notices archives and I found nothing. The subject was not in the area of interest of mathematicians. December 2008 issue of Notices is devoted to “Formal Proof”. It looks like formalized mathematics is going mainstream. There are four articles by Thomas Hales, Georges Gonthier, John Harrison and Freek Wiedijk. I am planning to discuss them here in the next couple of days.