This is a relatively large release with new material on algebra and algebraic topology contributed by Daniel de la Concepción Sáez. The full list of topics covered and not covered (yet) is in this GitHub issue. It will take some time before the new theory files are presented on the isarmathlib.org site, in the meantime they can be viewed in the standard Isabelle generated HTML presentation, the outline (definitions and assertions only) or the full proof document with proofs.

What is Zariski topology?

Let be the set of ideals of some commutative ring and be the set of prime ideals (i.e. the spectrum) of that ring. As it turns out the collection is then a topology, called Zariski topology.The carrier of this topology is and the closed sets are of the form for . So this notion belongs to algebraic topology but unlike for the topological groups or rings the topological structure is completely derived from the algebraic structure. Each ring has its Zariski topology.

Around 2007 at the beginning of the project I got an idea to speed up the development of the IsarMathLib library by importing theorems from Metamath’s set.mm. The theorems and proofs translated then are still a part of IsarMathLib and a small sample is presented at the isarmathlib.org site. After translating about 2000 proofs I decided to stop doing that as the work was repetitive and boring and the resulting proofs were not readable.

Metamath is considered a “low level” language and proof assistant, so I recently got curious how the Metamath proofs would compare with similar proofs written in the Isar dialect used in IsarMathLib. In this release I manually translated the Metamath’s utopreg theorem together with a couple of dependencies, taking advantage of Isabelle automation features to the extend I usually do in IsarMathlib. The following table compares verbosity of the original and translated proofs for the theorems whose proofs expressed similar ideas:

On average IsarMathLib proofs were about 2.3 times shorter. I have to say I expected that factor to be somewhere between 3 and 4.

The original Metamath utopreg theorem states that all Hausdorff uniform spaces are regular. After I translated the proof I was surprised to notice that the IsarMathLib’s version does not reference the hypothesis that the uniform space is Hausdorff. So, the IsarMathLib version shows that all uniform spaces are regular. I am not sure how it happened. To be honest I was not able to follow the Metamath proof exactly – it’s just too many small steps for me to put in my head at the same time. I was translating the proofs by first showing the steps marked green in Metamath Proof Explorer (I understand this indicates that the theorem referenced in the step is recent and hence close to the one being shown). Then I looked at facts made available this way and tried to figure out how one can get to the thesis of the theorem from them. It is possible that the Metamath proof does not make real use of this hypothesis as well, it’s just easier to spot in Isar.

I wrote the original isar2html tool 13 years ago in Haskell as a way to learn the language. Since then I was extending it and fixing bugs. Coming back once or twice a year to a language that I was not using professionally had quite a bit of overhead just to recall how the things worked and reconstruct the development environment. As it happened I changed jobs in April this year and the new job required F#, so I decided to rewrite isar2html in F#, again as a way to learn the language. Of course as usual with that type of “big rewrite” (well, not that big here really) projects I underestimated the effort needed so I finished only about a week ago. Now I have exactly the same application implemented the same way in Haskell i F#.

Haskell

F#

lines

2026

1692

words

10334

9239

characters

72006

79320

Basic verbosity statistics

The F# syntax is not as clean as Haskell’s so it was a surprise for me that the number of lines required was about 16% less in F# than in Haskell. Still, I would say that F# is slightly more verbose as the total number of characters was 10% higher in F#. Translating the parser of the subset of the Isar formal proof language that is used in IsarMathLib was almost mechanical and boring thanks to FParsec, which is the F# clone of Haskell’s Parsec parser library. I am especially happy with the result of that part of the project – the parsing errors were difficult to debug in Haskell. FParsec has better diagnostics built in – in case of failure it shows the backtracking information which helps a lot to pinpoint the problem in the text being parsed.

On the mathematics side in this release I have added a theorem stating that an ordered loop valued metric space is T_{2}.

This release updates IsarMathLib to Isabelle2021-1. There was actually not much to update – only a couple of places in the informal text that referenced Isabelle2021 now reference Isabelle2021-1. The main difference is in the HTML presentation that Isabelle generates from IsarMathLib sources. This presentation improved somewhat and now has links to referenced theorems in proofs. In one respect it is even better than the presentation at the isarmathlib.org site – the locale names in the statements of theorems are linked to the definitions, which is a feature missing on isarmathlib.org. I remember some statements by Makarius Wentzel on the Isabelle mailing list that the goal is the “publication quality” of officially generated HTML presentation. I hope that this includes what I think is needed the most – folding of structured proofs, support for mathematical notation with custom symbols and options for reduction of syntactic noise so that characters like the question mark or the quotes separating the object logic statements are omitted. When this happens I would be happy to retire the tool that generates isarmathlib.org HTML files. I wrote that tool 14 years ago with only a scant knowledge of HTML, CSS or Java Script and the web pages it generates are probably hopelessly old-style.

In other news, Pedro Sánchez Terraf announced that his team has completed a formalization of the independence of CH in Isabelle/ZF. This is a good news for IsarMathLib as well. Isabelle/ZF is used by very few people and I worry that at some point the Isabelle team stops supporting it, which would be the end of IsarMathLib. Every application like this makes it less likely.

Just to be clear, the loops in the title are algebraic structures and are not related to continuous images of circles or flow control constructs in programming languages.

Some time ago I got curious about a minimal setup in which a (pseudo) metric defined on a set would result in making this set a topological space. It turned out that if the metric is defined as a function with values in an partially ordered group we can use the standard definition of an open disk and the collection of unions of such open disks is a topology. However, I noticed then that this should be possible to be pushed a step farther and one should be able to define a metric as a function valued in an ordered loop and still get a topological space. In this release I added some material on ordered loops and rewrote the metric spaces section to be based on metrics valued in ordered loops.

Loops (the algebraic structures) are similar to groups, except that their binary operation does not have to be associative (I wrote more about loops in the previous post). An ordered loop (see for example Lattice-ordered loops and quasigroups by T. Evans) is a loop with a partial order such that if and only if and if and only if . The “if and only if” is worth noting here as this is different from the ordered group definition where one-sided implications are sufficient (I lost a couple of hours working with a wrong definition).

This release adds a theory file about loops. Loops (the kind we talk about here, not to be confused with for example loop algebras) are algebraic structures that are almost like groups, except that we don’t require the operation to be associative. Wikipedia has a nice picture illustrating dependencies between various algebraic structures between magmas and groups which I copy below:

As the picture shows we get a loop when we take a quasigroup and require that an identity (a neutral element of the operation) exists. It can be shown that that identity is unique in the loop. If we denote the loop identity as , then we can define the left and right inverses of a loop element as the only solutions to the equations and . In a loop these inverses do not have to be the same in general. If the loop operation is associative then we get a group and the left and right inverses unify to become the group inverse.

A quasigroup is a set with a binary operation (usually written with the multiplicative notation) that supports a certain kind of “divisibility”: every equation of the form or has a unique solution. So, a quasigroup is like a group except we do not require associativity or existence of a neutral element. If we denote those solution as and respectively we get the identities and by definition and, with the uniqueness, we get and , which may serve as an alternative definition of quasigroup.

According to this paper “One of the mathematical subfields where automated theorem provers are heavily used is the field of quasigroup and loop theory”.

In this release I added a new theory about real numbers. It’s mostly about setting up notation and validating other contexts (related to ordered fields, rings, groups, metric spaces etc.) so that theorems formulated in those contexts can be used when considering real numbers. At the end there are two theorems about the distance function being a metric and one stating that the collection of unions of open disks is a topology on reals.

IsarMathLib had been upgraded to Isabelle2021 in the previous release 1.16.1 (not announced on this blog) but at that time I didn’t notice that the proof documents were not generated properly. The pdf files generated by Isabelle didn’t get the formal text right, some symbols (like and , very important in mathematics based on set theory) were replaced by some placeholder symbol. Errors related to LaTeX are difficult to debug in Isabelle (at least for me), but this time I was lucky. The Isabelle2021 release notes contained information that the “The standard LaTeX engine is now lualatex, according to settings variable ISABELLE_PDFLATEX.” . Indeed changing the ISABELLE_PDFLATEX="lualatex --file-line-error" line in the settings file back to ISABELLE_PDFLATEX="pdflatex -file-line-error" like it was in Isabelle2020 fixed the problem.

I released the next version of IsarMathLib. This release adds a short theory file about lattices with definitions, notation and a proof that join and and meet-semilattices form idempotent () semigroups.

This version updates IsarMathLib to Isabelle2020. It was the easiest update ever – nothing had to be changed, so I just changed the abstract in the proof document with the project description.