Why Mathematicians Still Struggle to Define Equality in the Computer Age

Table Of Links

Abstract

1. Acknowledgements & Introduction

2. Universal properties

3. Products in practice

4. Universal properties in algebraic geometry

5. The problem with Grothendieck’s use of equality.

6. More on “canonical” maps

7. Canonical isomorphisms in more advanced mathematics

8. Summary And References

\ This paper has its origins in a talk [Buz] which I gave at Chapman University at the “Grothendieck, a Multifarious Giant” conference in 2022. Much of the paper was written in Coffee Zee, a coffee shop on the Holloway Road; I thank Seb for his excellent decaf oat cappucinos (even though I know he doesn’t approve). Many thanks to both Brian Conrad and the referee for their comments on a preliminary version. All remaining errors are solely the fault of the author.

Introduction

Six years ago, I thought I understood mathematical equality. I thought that it was one well-defined term, and that there was nothing which could be said about it which was of any interest to me as a working mathematician with a knowledge of, but no real interest in, the foundations of my subject. Then I started to try and do masters level mathematics in a computer theorem prover, and I discovered that equality was a rather thornier concept than I had appreciated. In particular I discovered that computer scientists had, many years ago, isolated several different concepts of equality, and had a profound understanding of the subject.

\ The three-character string “2 + 2”, typed into a computer algebra system, is not equal to the one-character string “4” output by the system, for example; some sort of “processing” has taken place. A computer scientist might say that whilst the numbers 2 + 2 and 4 are equal, the terms are not. Mathematicians on the other hand are extremely good at internalising the processing and, after a while, ignoring it. In practice we use the concept of equality rather loosely, relying on some kind of profound intuition rather than the logical framework which some of us believe that we are actually working within.

\ In fact we are far ahead of the computer scientists in these matters: the concept of mathematical equality (and in particular its usage in algebraic geometry to represent canonical isomorphism) is an idea which has not yet been captured by any of the formal definitions of the = symbol that we see in the literature or in computer theorem provers. The set-theoretic definition is too strong (Cauchy reals and Dedekind reals are certainly not equal as sets) and the homotopy type theoretic definition is too weak (things can be equal in more than one way, in contrast to Grothendieck’s usage of the term).

\ Mathematicians might claim to have captured some kind of “sweet spot” – but in fact, what I now believe is happening, is that we are using notational tricks to sweep various issues under the carpet rather than developing a more conceptual framework which would deal with them in a manner much more amenable to formalisation.

\ Fast forward to the present and I am still trying to do mathematics in a computer theorem prover (the Lean interactive theorem prover), rather than on pen and paper. I do this for the same reason that I write my papers in LaTeX rather than using a typewriter: I believe that it represents progress. Unfortunately, at the time of writing, the libraries of mathematics built in the various interactive theorem provers which currently exist are woefully inadequate for doing most modern mathematics.

\ However, over the last few years myself and hundreds of other mathematicians in the Lean community have spent many many thousands of person-hours building a digitised library mathlib ([mC20]) of standard undergraduate, Masters and early PhD level mathematics, so this is going to change. I hope that before I die, these computer tools will have matured to the extent that it is as easy to do mathematics in them as it is to currently do it on paper.

\ Once the systems are this mature, it might be the case that future generations of mathematicians will not have to worry about what people like Grothendieck mean by equality, because the systems will allow us to use the concept the way that it is currently used by mathematicians in practice. They will also point out to the author cases when it turns out that they didn’t fully perceive what they were doing (by pointing out possibly nontrivial issues which need to be resolved in order to make an argument complete).

:::info Author: KEVIN BUZZARD

:::

:::info This paper is available on arxiv under CC BY 4.0 DEED license.

:::

\