This new version updates IsarMathLib to Isabelle2019.

In related news, I have put the project on GitHub. I am planning to maintain IsarMathLib repositories both on the GNU Savannah and GitHub at least for some time.

Just another WordPress.com weblog

I gave a talk on IsarMathLib at the Third workshop on Formal Mathematics for Mathematicians (FMM 2018) on August 13. The workshop was part of 11th Conference on Intelligent Computer Mathematics (CICM 2018). The slides for my talk are available online on the CCIM page. The paper (an “extended abstract”) can be also found there, but they somehow cut the pictures from it, so it’s better to look at the original.

In other news I updated IsarMathLib to Isabelle 2018 which was released about a week ago.

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.

I updated IsarMathLib to work with Isabelle 2016 a couple of weeks ago. The distribution and the proof document are available in the usual places.

In other news, back in October 2015 Daniel De La Concepción, an IsarMathLib contributor, published an informal version of some of his contributions in a paper titled “New equivalences to axioms weaker than AC in topology”.

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

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.

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 isarmathlib.org 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:

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.

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.

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. (more…)