Archive for the ‘IsarMathLib releases’ Category

IsarMathLib updated to Isabelle2016-1

March 20, 2017

I finally got around to update IsarMathLib to Isabelle2016-1 that was released in  December last year. This was a quite time consuming update. The Isabelle system integrates LaTeX to be able to typeset well looking document proofs. This indeed works well – when it does. When there is a problem though it requires  LaTeX specific knowledge or long time to fix. This is what happened this time. The Isabelle team removed an element of its LaTeX setup that was obsoleted a couple of releases ago. They provided a script that was supposed to make necessary changes to theory files, but in my case running it on IsarMathLib’s 78 theory files just caused the errors to multiply. Fortunately Isabelle distribution sources provide lots of examples how LaTeX should be currently set up. After struggling for some time to understand the errors scattered over a 10MB log file I just created the IsarMathLib LaTeX setup from scratch following the examples and it worked. The IsarMathLib’s proof document and outline look better than ever.


IsarMathLib 1.9.3 released

June 30, 2015

This is a maintenance release to update IsarMathLib for Isabelle2015. There is no new formalized mathematics in this release.

IsarMathLib 1.9.2 released

October 20, 2014

I have released a new version of IsarMathLib – a library of formalized mathematics for the ZF logic of the Isabelle theorem proving environment. This is a maintenance release mostly to fix a couple of proofs that were not checking with Isabelle 2014 released at the end of August. The project distribution can be downloaded from the GNU Savannah server and the Isabelle generated proof document provides information on all theorems formalized by the project. The outline document is a shorter version of that without proofs.

IsarMathLib version 1.9.1 released

January 3, 2014

This is a maintenance release mostly to update IsarMathLib to Isabelle 2013-2. The RIPEMD-160 hash (a2ef972973bb2d072c7702d28dcfabee9026bd3b) of the proof document for this release is timestamped in the Bitcoin blockchain at 1FrXV7eifF2zruVr8YHJdvV8GHucUAqxYy.

IsarMathLib 1.9.0 released

July 26, 2013

I have released version 1.9.0 of IsarMathLib. This is a quite large release with 10 new theory files and 155 new theorems, all contributed by Daniel de la Concepción Sáez. The first of the files contributed by Daniel (released in 1.8.0), Topology_ZF_4 about nets, filters and convergence in topological spaces is now presented on the site. The rest of Daniel’s contributions for now can be viewed in the proof document and the outline.

Here is a short description of what is in the new theories:


IsarMathLib 1.8.0 released

February 25, 2013

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 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 (x_0, x_1,...,x_{n-1})\mapsto \sum_{i=0}^{n-1}x_i is continuous in the natural topology on the space of n-element sequences of a topological group.

IsarMathLib 1.7.5

October 9, 2012

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

June 30, 2012

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 (x_0, x_1, ..., x_{n-1}) \mapsto \sum_{i=0}^{n-1}x_i is continuous on G^n where (G,+) is a topological group. This will be my goal for the next release. (more…)

IsarMathLib 1.7.2

July 20, 2011

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:

\overline{A} = \bigcap_{H\in \mathcal{N}_0} A+H

Here, \mathcal{N}_0 is the collection of neighborhoods of zero (sets whose interior contains the neutral element of the group), and for two sets A,B\subseteq G we define A+B as A+B=\{a+b | a\in A, b\in B\}.


IsarMathLib 1.7.1

May 13, 2011

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 K\times K\setminus \{0\}, 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 (X_1,\tau_1) and (X_2,\tau_2) and we partition X_1 into two sets U,V\subseteq X_1, \ U\cup V=X_1, both open (or both closed), and a function f:X_1\rightarrow X_2 is continuous on both U and V, then f is continuous. The version in IsarMathLib is bit different, stating that the collection of open sets \{U \in \tau_1 : f|_U \text{is continuous}\} 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 \{U \in \tau_1 : f|_U \text{is continuous}\} forms a topology, \emptyset belongs to it, i.e. f|_\emptyset is continuous. But f|_\emptyset is in fact \emptyset 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.