IsarMathLib 1.8.0 released

I have released the 1.8.0 version of IsarMathLib. This version works with the new Isabelle2013 (released about two weeks ago). The new material in this release mostly comes from contributions by Daniel de la Concepción Sáez, who added 5 theory files with about a hundred theorems about general topology. The subjects range from convergence of nets and filters and related continuity properties of functions, through some generalized notions of compactness and connectedness, to rather abstract (like, category theory abstract) subjects of heredity and spectra of topological properties. Unfortunately, it will take some time before those theories will be presented on the FormalMath.org site, as my parser is not good enough to parse Daniel’s advanced Isar style.  I will work on this though and in the meantime an interested reader can have a look at the Isabelle generated full proof document or the outline.

As for myself, I have finished the proof that the function is continuous in the natural topology on the space of -element sequences of a topological group.

IsarMathLib 1.7.5

The 1.7.5 version of IsarMathLib has been released. The new formal math there consists of two theory files contributed by Daniel de la Concepción Sáez with over 70 theorems about various examples of topological spaces.

IsarMathLib 1.7.4

I have released version 1.7.4 of IsarMathLib. The new formal math there is a mostly in the Topology_ZF_3 theory about  topologies on function spaces. This is needed to show that the function is continuous on where is a topological group. This will be my goal for the next release.

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.

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.

Isabelle 2009-1 and IsarMathLib

The Isabelle team has just released Isabelle 2009-1. The latest release 1.6.9 of IsarMathLib checks out without any modification, so there is no update needed.

The new installation instructions on the Isabelle web site and the bundle file that can be downloaded from there are specific for Isabelle/HOL. To install Isabelle/ZF for IsarMathLib on x86 Linux one needs to download Isabelle2009-1.tar.gz, polyml-5.3.0.tar.gz,  ProofGeneral-3.7.1.1.tar.gz and ZF_x86-linux.tar.gz and do tar -C /usr/local -xzf on each of them. The installation can be finished by running

./bin/isabelle install -p /usr/local/bin

from /usr/local/Isabelle2009-1.

IsarMathLib version 1.6.9 released

I have released a new version of IsarMathLib. There are about 20 new theorems and a new theory on topological groups. The theory contains some basic definitions and notation and ends with a theorem that a subgroup of a topological group is a topological group.

IsarMathLib version 1.6.8 released

This release is  the first version of the IsarMathLib library for the new Isabelle2009. There is a little bit of new formalized mathematics as well.