Recently read

I haven’t updated this blog for a while, so I decided to try to break the writer’s block by posting a couple of quotes from the formalized mathematics stuff I read recently.

There was a discussion initiated by James Frank in November last year on the Isabelle mailing list about problems with making mathematics formalized in HOL similar in notation and terminology to the standard (informal) mathematics. The main difficulty here is that standard mathematics uses set theory notation, so obviously something based on type theory has to look different. This lead to a discussion what might be the reasons of doing formalized mathematics in simply typed HOL rather than set theory. Josef Urban expressed the following opinion:

I do not think that there are good pragmatic automation-related reasons for persuading mathematicians to work in HOL instead of ZF. Given the very low penetration that formal mathematics has so far among mathematicians, I think it would not hurt the formal systems to go where the mathematicians are.

with which I fully agree.

In the same thread Steven Obua announced the ProofPeer project – a cloud-based social network interactive theorem proving system. (That is probably the the highest concentration of buzzwords in one sentence that I ever wrote.) The alpha launch is planned for summer 2012. He recently published a paper with more details about ProofPeer.

On the subject of types vs. sets as a foundation I recall a funny cartoon that I found on a LtU thread related to this.

Back in 2008 Freek Wiedijk wrote a nice article on “Formal Proof—Getting Started”. Here is my favorite part of it:

In mathematics there have been three main revolutions:

• The introduction of proof by the Greeks in the fourth century BC, culminating in Euclid’s Elements.
• The introduction of rigor in mathematics in the nineteenth century. During this time the nonrigorous calculus was made rigorous by Cauchy and others. This time also saw the development of mathematical logic by Frege and the development of set theory by Cantor.
• The introduction of formal mathematics in the late twentieth and early twenty-first centuries.

Frank Quinne’s article “A Revolution in Mathematics? What Really Happened a Century Ago and Why It Matters Today” in  the January issue of Notices of the AMS is devoted to the second revolution. Here is a quote:

As the transition progressed, the arguments became more heated but more confined. At the beginning traditionalists were deeply offended but not threatened. But because modern methods lack external checks, they depend heavily on fully reliable inputs. Older material was filtered to support this, and as the transition gained momentum some old theorems were reclassified as “unproved”, some methods became unacceptable for publication, and quite a few ways of looking at things were rejected as dangerously imprecise. Understandably, many eminent late nineteenth-century mathematicians were outraged by these reassessments.
Meanwhile, very high reliability has been achieved in mathematics without drawing attention or having significance attached to it. The axiomatic-definition approach also made mathematics more accessible. A century ago original research was possible only for the elite. Today it is accessible enough that publication is required for promotion at even modest institutions, and an original contribution can be required for a Ph.D.

It is striking for me how well this describes the situation with the third revolution. The analogy extends also to the sort of democratization of mathematics that machine verification makes possible.

IsarMathLib 1.7.2

I have released a new version of IsarMathLib. It adds about 50 new lemmas, mostly in group theory and topology, leading to the following characterization of closure in topological groups:

Here, is the collection of neighborhoods of zero (sets whose interior contains the neutral element of the group), and for two sets we define as .

IsarMathLib 1.7.1

I have released version 1.7.1 of IsarMathLib. There are two small topics I added, both in the “weird math” category.
The first is related to the “1/0=0″ story that I talk about in another post. Proving the theorem that states that was a little bit more involved that I had thought. I had to define the notion of division in fields as a function on , then notation for it. I don’t think I cheated here but the truth is I did make an effort to make the theorem look like the one I wanted to prove. This brings up the question: what if I made a little more effort and manipulate notation so that a theorem appears to mean something different that it really does? For example it is quite easy in Isabelle to change the notation to print “True” as “False” and prove a theorem that appears to show inconsistency in ZF.
Freek Wiedijk’s paper formalizes this question. Back in January there was also a long thread on the Isabelle mailing list where people expressed varying opinions on how serious the problem is.

Another small piece of formal math that I added in this release is a chapter in the Topology_ZF_2 theory on the pasting lemma. The classical pasting lemma states that if we have two topological spaces, say and and we partition into two sets , both open (or both closed), and a function is continuous on both and , then is continuous. The version in IsarMathLib is bit different, stating that the collection of open sets forms a topology.
Surprisingly from this we can conclude that the empty set (which in ZF is the same as zero of natural numbers) is continuous. Here is how it happens: since the collection forms a topology, belongs to it, i.e. is continuous. But is in fact and we get that zero is continuous. Ha Ha.
I would like to emphasize that I do not consider facts like this as demonstrating that ZF set theory is not a suitable foundation for formalizing mathematics (as some people interpret). It is just fun and games that formal math allows and I am sure other foundations also have their unintuitive corner cases.

The first formalized math wiki is here

I have been wondering for a couple of years who will be the first in the race to set up a a publicly available, working and usable formalized math wiki. Now ladies and gentlemen we have the winner and the winner is Wikiproofs.org!

Isabelle2011, IsarMathLib 1.7.0 and other news

Isabelle team has released Isabelle 2011. The upgrade was not as smooth for me as the previous one. The new ProofGeneral didn’t work with Xemacs shipped with Ubuntu 9.10, giving a “file mode specification error”. I tried then the new jEdit interface that found that ZF logic is missing. Indeed, the Linux bundle does not contain precompiled ZF logic. It was not a big problem, I built it with “build ZF”.

The jEdit interface  (see the screenshot)  represents a new approach based on “continuous proving” concept. While I think it is very interesting technologically, it turned out extremely slow on my Athlon 64 1.8GHz with ony 512MB of RAM. Apparently all this proving in the background with keeping multiple versions of the document was just too much. It would be usable if it was possible to temporarily disable the continuous proving feature, but unfortunately this is not supported yet.

The next generation of proof assistants: ten questions

Checking for new stuff on Freek Wiedijk’s home page I stumbled upon slides of his recent talk given on Workshop on Logical and Semantic Frameworks in Natal, Brasil. He poses there ten questions about how the next generation of proof assistants should look like. In this post I want to give my answers to those questions.

Should the next generation of proof assistants be based on ZFC set theory?

New versions of Isabelle, I3P and IsarMathLib

A new version of Isabelle was released on June 23rd. This version is called  Isabelle2009-2 which I find bit strange in 2010.The standard installation is simple and includes the ZF logic. To work with IsarMathLib it’s probably a good idea to change the ISABELLE_LOGIC prameter in etc/settings to ZF.

The changes in the new version are related mostly to HOL. There is a small change in naming of some environment variables, so I released IsarMathLib 1.6.10 to make sure the library checks out of the box by typing “isabelle make”. This IsarMathLib version contains no new formalized mathematics.

Isabelle2009-2 contains “the preliminary Isabelle/jEdit application demonstrates the emerging Isabelle/Scala layer for advanced prover interaction and integration”. Here is a screenshot of the editor showing TopologicalGroup_ZF theory.

The new jEdit based Isabelle interface

The display of the Isabelle math symbols is flawless. The subscripts (\<^isub> in source) are not displayed though.

I was unable to use this as an actual interface to Isabelle. When I select “Plugins/Isabelle/Activate current buffer” the colors change somewhat. From the ps output it seems that Isabelle process starts, but there is some kind of failure in lib/scipts/feeder.pl. I couldn’t do anything else. I didn’t try too hard though.

Following the Isabelle release a new version of the I3P interface was relesed as well. There is some improvement in rendering math symbols possibly because of improvement in the Isabelle font. However the display of symbols is still not reliable. Some symbols (like \<tau>) are rendered correctly in some places but not others. Some, like \<langle> and \<rangle> are not displayed at all. This is not a problem with Isabelle fonts as the jEdit based interface displays those symbols correctly. The subscripts are also not rendered as such.

How to Publish Counterexamples in 1 2 3 Easy Steps

I found some time to look over recent issues of Notices of AMS and I noticed a letter from Theodore P. Hill, a mathematician from Georgia Tech. The letter led me to read his article “How to Publish Counterexamples in 1 2 3 Easy Steps”. It’s a story that starts when he found errors in a mathematical paper that he got for review and traced those errors to a previously published article in Notices and ends almost two years later in pretty much a complete failure to cause any public admission of the problem and correction from the authors.

Goodbye ProofGeneral, again

A couple of weeks ago Holger Gast announced the first release of the new interactive interface for Isabelle theorem prover. I was planning to write its review, but I decided not to as Jesus Aransay’s wrote a post on the Isabelle mailing list that  pretty much summarizes what would be in that review.

For me the lack of proper display of mathematical symbols and subscripts is a show stopper. You can’t write mathematics without that. I hope that will be resolved soon and I3P will be an excellent replacement for ProofGeneral.

Gödel, Chaitin and formalized mathematics

The subject of formalized mathematics has shown up in Slashdot discussions a couple of times. Every time that happened someone mentioned Gödel inconsistence theorems and from that point on much of the discussion concentrated on how Gödel results imply (or not) that formalized mathematics is impossible, impractical or useless.

When I see a discussion like this I think how some seventy years ago a similar forum would discuss the idea that it would be possible and useful to do away with human computers and use machines to execute algorithms. There would be similar arguments about how you could not do that because to execute an algorithm one has to understand it first and machines can not uderstand anything. The art of designing algorithms would lose its beauty when the algorithms would have to be written in a machine language. And, due to a deep theoretical result called the “halting problem” we would have no way to know in advance if such algorithm would ever stop to produce a useful result.

It is easy to dismiss  Slasdot discussions and blame them on the general cluessness of the Slashdot crowd. However, I recently stumbled upon the text of a talk given by Chaitin at the University of Cordoba in November last year that completely puzzled me.