There are three approaches to defining uniform spaces. The first one, through *diagonal* *uniformities* is presented in IsarMathLib in the UniformSpace_ZF theory. This release adds a theory about defining uniform spaces through *uniform covers*.

Consider a set with its powerset (the set of subsets) . A collection of subsets of whose union is equal to is called a *cover* of . So, we can define the set .

For a set and a collection of of subsets of we can define the *star* of *in* as .

For two covers we say that the cover is a star-refinement of the cover and write if for every we can find a such that is contained in .

Finally we are able to define uniform covers. This notion is a bit tricky as there is really no separate notion of a uniform cover. If we look at cover of we cannot say if this is a uniform cover or not. What actually is defined is a *family* of uniform covers. A member of such family can only be called a uniform cover if it is clear from the context what family of uniform covers it belongs to.

A nonempty collection of covers of is called a *family of uniform covers* iff the following two conditions hold:

a) If , and , then

b) For every two covers we can find a cover that is a star-refinement of both and

This definition is slightly different that the one on the Wikipedia page on uniform spaces, which specifically requires that the trivial cover is a member of . However, since every cover is a star-refinement of the trivial cover and is not empty, condition a) implies that .

The key fact here is that if is a family of uniform covers of then the following collection of subsets of is a (diagonal) uniformity:

In words, is the collection of supersets of sets of the form as ranges over .

In Willard’s “General Topology” book the proof that is a uniformity is left as a “straightforward exercise” for the reader. Typically that means that the proof is long and tedious and the author does not feel like typing all that down. In this case the proof is indeed of mostly straightforward “follow your nose” kind right up to the moment when given a set one needs to find a set such that (here is the composition of relation with itself). For that, I found the following identity useful:

It took me some effort to figure out this identity and I was ready to type the proof of that in Isabelle, split into two inclusions etc. To my amazement though Isabelle accepted this fact without an explicit proof, only with the reference to the definition of star. This was probably the most unclear to me fact that was obvious to Isabelle that I have seen writing proofs for IsarMathLib so far. I left the proof of this identity as an exercise for the reader. This time the straightforwardness of this fact got certified by Isabelle.

Which brings us to the subject of

## Automation in proof assistants

Ok, it’s grandfather’s story time. Long time ago and far away, when I was studying mathematics at the University of Tennessee, Knoxville, there was a very talented student from Romania there, let’s call him Gabriel P. Once I was struggling with a proof of some theorem and I asked him if he has an idea how to prove this thing. He looked at the problem, thought for a minute, then nodded his head, smiled and said “It’s true”. And left. I was more frustrated than enlightened and since then I am of opinion that automation in proof assistants is overrated.

Sure, automation is good for the writer as it reduces their effort. However, if there is too much of automation it affects the reader as it reduces the amount of information contained in the proofs. So there is a trade off with some optimum depending on writer’s goals. If the writer goal is certification of truth only, as is usually the case with software verification, then the more automation the better. In mathematics the issue of communication comes into play and the proofs are supposed to convey information on *why* an assertion is true.

Of course ideally the proofs would be built by a dialogue between a researcher and a proof assistant AI. The PA would then generate readable proofs in a structured proof language that processed by the presentation layer would allow a reader to set their desired level of detail, from high level bullet points down to the Metamath-style atomic steps. A couple of days ago I considered proof assistants like this such a remote possibility that it would not be worth it to even write this paragraph. This changed after I saw the Open AI Codex demo. I think now that proof assistants that do for crafting formal proofs what Open AI Codex does for programming are a couple of years off, at most.

Tags: formalized mathematics, IsarMathLib releases, proof assistants

## Leave a Reply