IsarMathLib version 1.16.0: metric spaces

February 1, 2021

In this release I added a new theory on (pseudo-)metric spaces. Daniel de la Concepción Sáez contributed a theorem stating that in topological groups the group inverse is uniformly continuous with respect to the Roelcke uniformity.

A pseudo-metric is typically defined as a function d: X\times X \rightarrow [0,\infty) that satisfies the conditions d(x,x) = 0, d(x,y) = 0 \Rightarrow x=y and d(x,z) \leq d(x,y)+d(y,z) for all x,y,z \in X. This is sufficient to prove that the collection of subsets of X that are unions of disks (defined as \text{disk}(c,r) = \{x\in X: d(c,x)<r\}) is a topology, making this metric space a topological space. If we replace the interval [0,\infty) in the definition of pseudo-metric by the nonnegative set of a linearly ordered, abelian, Archimedean group then we are not changing anything as such group is isomorphic to a subgroup of the additive group of real numbers. I was curious: what is really needed to get a topological space from a pseudo-metric space this way? Do we really need the group to be Archimedean? Does the group operation have to be commutative? Do we need the order to be total? Amusingly, the answer to these questions is “no”. The group does not have to be abelian and the Archimedean property is not needed. The linear order condition can be relaxed by assuming that the positive set is a meet semi-lattice (every two-element subset has a greatest lower bound) under the group order relation. I don’t know if this is useful to know, but surely my personal curiosity got satisfied.

IsarMathLib version 1.15.0: comparison with Mizar

December 13, 2020

Some time ago Victor Makarov asked on the Mizar forum about two theorems in group theory. The first theorem states that the union of two subgroups is a subgroup iff one of the subgroups is a subset of the other subgroup. The other one gives a criterion for when for two subgroups H,K the set H\cdot K = \{x\cdot y | x\in H,y\in K \} is also a subgroup. These theorems turned out not to be in the Mizar Mathematical Library, but Roland Coghetto posted formalization of those two theorems in the Mizar proof language. In this release I added the formalization of those two theorems to IsarMathLib so that one can easily compare the syntax and style of Isabelle’s Isar proof language (as it is used in IsarMathLib) and the Mizar proof language.

The result can be viewed as theorems named union_subgroups and prod_subgr_subgr. For the proof of the first one I followed the informal source on Stack Exchange provided by Roland, so it can be directly compared to its Mizar version. The proof of the second one is probably different than the Mizar version, but I think they are still useful as examples of the same theorem in different proof assistants.

IsarMathLib version 1.14.0: lattices

September 29, 2020

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 (x\cdot x = x) semigroups.

IsarMathLib version 1.13.0: Roelcke uniformity

August 3, 2020

I have released version 1.13.0 of IsarMathLib. This release adds the definition and basic properties of the Roelcke uniformity, contributed by Daniel de la Concepción Sáez.

So, what is Roelcke uniformity? As we all know each topological group is a uniform space with two natural uniformities: the left uniformity and right uniformity. The collection of uniformities on a set forms a lattice (in fact, a complete one) so it is natural to ask what are the meet and join of the left and right uniformities. The meet is called the Roelcke uniformity. More details with references can be found in answers to this StackExchange question and the formalization is available in the IsarMathLib’s TopologicalGroup_Uniformity_ZF theory.

 

IsarMathLib version 1.12.1: update to Isabelle2020

May 12, 2020

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.

IsarMathLib version 1.12.0: topological groups and uniformities

May 5, 2020

This release adds three theory files contributed by Daniel de la Concepción Sáez. Two of them, Topology_ZF_properties_2 and Topology_ZF_properties_3 have been in IsarMathLib for a long time, but I forgot to add them to the file that lists theories to be presented, so they were not showing up in the Isabelle generated HTML presentation or the proof document. Now they do.

The third theory TopologicalGroup_Uniformity_ZF (see also the section Topological groups – uniformity in the proof document or the outline) is brand new in this release and contains a proof that  every topological group is a uniform space.

IsarMathLib version 1.11.0: uniform spaces

February 11, 2020

I have released the next IsarMathLib version both on the GNU Savannah server and the IsarMathLib’s repository on GitHub. This release adds a theory about unifom spaces.

IsarMathLib version 1.10.0: neighborhood systems

November 23, 2019

This release adds a short theory on neighborhood systems in topological spaces. Besides the usual places for the sources, proof document and the outline on the GNU Savannah server one can download those from the GitHub mirror.

Years ago I had a plan to formalize some notion of measure and integration that would be different and perhaps more general than the usual Borel/Lebesque measure.  I recently came back to this and searched a bit what is known about measures and integration taking values in topological groups. One of the things I found was a story about Grothendieck’s manuscript titled “L’intégration à valeurs dans un groupe topologique” that he presented to Dieudonné when he arrived to the University of Nancy to become a doctoral student there. The paper was harshly criticized by Dieudonné for its “reprehensible tendency to gratuitous generality” (I love gratuitous generality). The manuscript is now lost for ever probably.

On the measure side of things I found an old (1973) bookA Theory of Semigroup Valued Measures”  by Maurice Sion and some earlier papers on the subject. The Google preview of the book suggests that the setting considered there are topological semigroups. This notion depends on uniform spaces, which depend on neighborhood systems, hence the the subject of new theory in this release.

For the integration I found an interesting paperLattice Valuations: a Generalisation of Measure and Integral” by  Bram Westerbaan. This presents a unification of the notions of measure and integral under a common notion of lattice valuations (that would be a gratuitous generality again I guess). This is done in the setting of (partially) ordered abelian (topological) group. From my point of view I was kind of hoping that someone has come up with a way to define say SO(3) valued measures, or at least SO(2) if we really need the group to be abelian.

There is also the paper “Notes on Lebesgue integration” by Gyula Lakos that I had known before. This one is written is style that is very difficult to formalize and assumes that we already have measures.

Lean and Metamath Zero

November 10, 2019

It seems there is a wave of interest in formalized mathematics among professional mathematicians, driven by a very successful Lean mathlib project. There is a video of Kevin Buzzard’s talk about the project and an arXiv paper describing it. Kevin Buzzard is an algebraic number theorist and a professor of pure mathematics at Imperial College of London. In the summer 2018 he led a summer project with twenty undergraduates that were were learning Lean and formalizing mathematics in it. He also sometime uses Lean live coding while teaching classes and runs a Lean club at Imperial called the Xena Project. His article in the London Mathematical Society newsletter provides more info on this.

Lean is a programming language and software verification tool from Microsoft Research. I think Thomas Hales’ review is the best source on its strengths and weaknesses from the formalized mathematics point of view. Lean’s logic is calculus of inductive constructions (CIC, similar to what Coq is based on). So Lean mathlib formalizes mathematics in (dependent) type theory. Of course  this is a bit unfortunate from my point of view as I am more of a set theory person. There is no doubt though that type theory is nowadays more popular (not to say successful) foundation in formalization efforts. Jeremy Avigad wrote a rare compelling explanation of why this is the case.  I personally prefer the opinion of Lawrence Paulson, the original author of Isabelle and its ZF logic (he also implemented a formalization of ZFC set theory in Isabelle/HOL recently). Here is what he says:

I would guess that the amount of effort and funding going into type theory exceeds the amount that went into set theory by an order of magnitude if not two. It’s not unusual to encounter open hostility to set theory and classical logic combined with an air of moral superiority: “Oh, you aren’t constructive? And you don’t store proof objects? Really?” And I have seen “proof assistant” actually DEFINED as “a software system for doing mathematics in a constructive type theory.

The academic interest simply isn’t there. Consider the huge achievements of the Mizar group and the minimal attention they have received.(…)

I am certain that we would now have highly usable and flexible proof assistants based on some form of axiomatic set theory if this objective had enjoyed half the effort that has gone into type theory-based systems in the past 25 years.

In January 2020 there will be a conference on Formal Methods in Mathematics and Lean in Pittsburgh, Pennsylvania.

Another project related to formalized mathematics that I think is very interesting is Metamath Zero by Mario Carneiro. This is a formal proof verifier, heavily inspired by Metamath, but with a different architecture, some improvements in the metalogic and the ambition to be a “bootstraping theorem prover”, i.e. be able to verify itself. The details are in the arXiv paper, but below is the summary of what I think I understood from it.

Metamath Zero (MM0) separates the specification from the proofs, so there are two inputs to the verifier. The specification is a human readable text written in mm0 language which is as generic as the Metamath language, i.e. it can specify  logics from ZFC on FOL, through Quantum Logic(s), type theories like HOL or CIC, to the Intel x86 instruction set architecture. Anything, really. The proofs are provided separately in a binary whose format (mmb) is optimized for verification speed. This is the format that allowed MM0 to verify the material contained in the Metamath’s set.mm with its 23000 proofs in 195 ms on Intel i7 3.9GHz (the previous record was 0.7s). This part of the architecture can serve as independent backend of any theorem prover that is able to provide the mm0 specification and mmb proof binary.

An example of such theorem prover is included in the MM0 system, together with a proof language mm1 (similar to mm0) and an formal text authoring tool as a Visual Studio Code plugin implementing Language Server Protocol.

I don’t want to write about the MM0 metalogic as there is too much risk to say something wrong here. I only want to mention that the paper contains a very clear explanation of Tarski-Megill metalogic (used by Metamath) that replaces the notion of free and bound variables by the notion of distinct variable groups.

The bootstraping goal which I understand is work in progress consists of specifying Peano Arithmetic, then x86 instruction set architecture and the formal system of MM0 to get a complete specification of the working of the ELF binary file that executes the verifier.

IsarMathLib version 1.9.8 released

August 29, 2019

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.