Two types of universe for two types of mathematician

Thank you Johan for pointing out to me that the mathlib stats page had got really good! But one thing that made me laugh is that somehow on their stats for commits

I see I have done just enough to get a mention! I was quite surprised. Let’s look at those mathlib committers, most of them far more prolific than I am. Who are they? One surprising thing about them: although we have a common goal, of formalising mathematics in Lean, we are a really mixed bag of people, some of whom you might expect to have no research interests in common with me at all.

Yury Kudryashov is a post-doc in the maths department at Toronto. I’ve never met him, because of visa issues. The dark blue line shows his meteoric rise.

Scott Morrison does TQFT‘s at ANU and was one of the founders of MathOverflow.

Mario Carneiro is a PhD student of Jeremy Avigad, in the philosophy department at CMU. He taught me Lean.

Johannes Hoelzl is a computer scientist who works for Apple on formally verifying their products. He wrote the filter library for mathlib, which was essential for Patrick Massot’s work on topology, in turn crucial for the construction of perfectoid spaces in Lean.

Chris Hughes is an undergraduate at Imperial College London. He’s going to an MSc project with me next year, on a one-relator group tactic. Chris has taught me so much about what mathematics really is. Chris learnt Lean when he was a 1st year undergraduate and began to interpret all of his lectures from a type theoretic point of view, which in turn has led to what I think is an extraordinary understanding of “what is actually going on” in a pure mathematics undergraduate degree (in particular exactly how informal some of it is).

Rob Lewis has a PhD in logic and is now a post-doc in the computer science department at VU Amsterdam. He wrote linarith (“Loves the jobs you hate”). I ran into serious technical problems with tactics malfunctioning when making the natural number game, and Rob wrote the code which enabled me to hack tactic mode and fix stuff, saving the project. He set up the mathlib documentation project. This is the community’s effort to explain Lean’s interface to mathematicians. Before his academic career, he was a teacher.

Sébastien Gouëzel is a professor of mathematics in Nantes, who won the Brin Prize in 2019. He was the driving force behind manifolds in Lean. We now have C^n and C^\infty manifolds, over general complete fields such as the complexes, reals or p-adics, and in the real case you can also have corners. It was harder than you might initially think.

Johan Commelin is a post-doc in arithmetic geometry in Freiburg, working with Annette Huber. He has a wife and three small kids, and last week uploaded not one but two papers to ArXiv about o-minimality. He developed the API for a new Lean type called a “group with zero”, for example a field or a division ring but forget about the addition. Talking to him about stuff like this made me understand that the definition of a UFD never uses addition, and is hence a special case of a more general definition. History sometimes needs rewriting, but it’s OK — we hide the details from you. A UFD is a monoid with zero, by the way (such that the underlying monoid is a product of a group and a free abelian monoid — that’s the full definition in fact, although there are two ways of interpreting “is”).

Simon Hudon is a computer scientist and an excellent functional programmer. His definition of a monad is different to mine, and he knows what all the weird >-> symbols mean. He wrote a bunch of stuff in core Lean and was around since the start. Mostly meta.

Patrick Massot has translated most of Bourbaki’s Topologie générale into Lean, and can now confirm that they were (almost always) right. He’s a topologist in Orsay (except now we say Saclay) and teaches his undergraduates using Lean. You should try his introductory analysis problem sheets and other stuff in the Lean Tutorials repo. If you have Lean installed the modern way, you can just type leanproject get tutorials and then open the project in VS Code. Patrick also wrote the leanproject tool, and it has solved the constant problems beginners on Windows machines were having when trying to get a fully compiled mathlib running locally without waiting an hour or more for it to compile.

Reid Barton won four gold medals at the IMO.

Kenny Lau is an undergraduate at Imperial College, whose first year project on formalising the statements of local class field theory for abelian algebraic groups in Lean unsurprisingly won the “best pure maths project of the year” prize. I needed localisation of rings when doing schemes and he bashed out the entire theory like it was easy.

Gabriel Ebner is our bald-headed fixer. If the mathlib people can’t get something to work and they blame Lean, he sometimes has words with it directly. He has driven Lean from 3.4.2 to 3.17.1 in the space of, what — six months? It’s better and it’s faster. To anyone still on Lean 3.4.2 — switch to the Lean Prover community version of Lean. It’s so much easier now. Anyone searching for Lean — beware of Microsoft’s old pages. Search for Leanprover community or mathlib.

And then me at the bottom. A professor of maths with a general malaise about the state of number theory, who three years ago this week tried Lean for the first time and got hooked.

We’re a really motley crew, talking to each other about different ways of thinking about common areas of interest. There are many other people who have committed to mathlib too — e.g. people I’ve met on discord whose names I don’t even know but who got interested in seeing if they could formalising a random thing in Lean, and it has turned out that the answer is “yes, and in doing so you can make mathlib better”. People like Amelia Livingston, another Imperial undergrad, who felt that Kenny Lau’s theory of localisation of rings should be generalised to localisation of monoids and rewrote the whole lot. She was right. People like Shing Tak Lam, who was practicing for his STEP exams (hard UK school maths exams for 18 year olds) by formalising the questions, and his project to formalise a question about polynomials over the reals from STEP ended up with him developing the entire mathlib theory of partial derivatives for multivariable polynomial rings. He asked what a ring R was at some point, I said “just pretend it says the real numbers \mathbb{R}“.

The two cultures of mathematics

Together we are investigating the boundary between the specification of mathematics, and the implementation of mathematics, for both definitions and for proofs. I learnt from Sébastien at LFTCM2020 that we can now prove that smooth morphism of smooth manifolds induces a morphism on tangent spaces in a manner functorial in the manifold, but it took a bunch of people to turn the theorem statement from maths into code, and then a bunch of people to translate the proof from maths into code (and everyone was standing on the shoulders of giants, in some sense).

There are two universes involved in what we are making. There’s the part that’s in Type (where the creative ideas such as perfectoid spaces and the Cauchy reals are digitised) and Prop (the part within the begin/end blocks where the computer games are). In Tim Gowers’ essay on the two cultures of mathematics, he talks about the concepts of theory-building and problem-solving. I have always believed that there was something very true at the core of this, but now I am beginning to understand it much better. Type is where the theory-building is going on, and Prop is where the problem-solving is occurring.

But these two parts of mathematics are inextricably linked. Patrick, Johan and I formalised the definition of a perfectoid space, but on the way there we had to prove a whole load of theorems — even before we could write down the definition. There are two topologies on an affinoid perfectoid space. One generated by basic open subsets, and one generated by rational open subsets. In the future, when defining sheaves on a perfectoid space, sometimes we will use one basis, and sometimes the other. The proof that they are the same is 20 pages of very tricky algebra involving valuations on topological rings, and we have not done it yet — we just picked one of the definitions when defining a perfectoid space and moved on. At some point in the development, we will need to use the other definition, and then we’ll have to prove the theorem. But in fact this sort of thing already happened to us many many times before, and then we did have to prove the theorems. Sometimes things get tough. Mathematicians so good at instantly switching between the various “obviously equivalent” ways that a mathematician looks at a complicated algebraic object (“It’s an equivalence relation! Now it’s a partition! Now it’s an equivalence relation again! Let your mental model jump freely to the point of view which makes what I’m saying in this particular paragraph obvious!”, or “Matrices are obviously associative under multiplication because functions are associative under composition.” (dutiful student realises later that this proof assumes the action of matrices on \mathbb{R}^n is faithful, and did you see that dependent type there?). Some of the proofs we’re writing are simply proofs that humans are behaving correctly when using mathematical objects.

But writing some proofs in mathlib is just fun. In fact there are now a growing number of proofs in Lean written by mathematicians who are coming to mathlib and finding that the interface to the thing they wanted (e.g. a topological space, or an equivalence relation, or a ring) is there and usable. It is hence possible for them to state and prove (or reprove, if mathlib did it already) the results they are interested in, using Lean’s tactic framework. We don’t know how far this can go, and we don’t know whether type-theoretic issues will cause problems further down the line (e.g with etale cohomology) but at this rate, it looks like we’re going to find out.

Currently on display at Royal Academy of Art (proud Dad :-))

About xenaproject

The Xena Project aims to get mathematics undergraduates (at Imperial College and beyond) trained in the art of formalising mathematics on a computer. Why? Because I have this feeling that digitising mathematics will be really important one day.
This entry was posted in Uncategorized and tagged , , . Bookmark the permalink.

7 Responses to Two types of universe for two types of mathematician

  1. Tom Leinster says:

    Hi Kevin. I’ve read quite a few of your posts on this blog and seen you speak about Lean, but I don’t remember ever hearing you explain your “general malaise about the state of number theory”. I’d be interested to hear it.

    Like

    • xenaproject says:

      One reason I initially got interested in Lean because I was concerned about the degree of rigour which was now acceptable in modern number theory, including things such as “we assume a result which X announced ten years ago and said they would write up, but never did”. Now I understand that theorems provers cannot really solve this in their current state, but I still don’t want to go back.

      Like

  2. David Corfield says:

    Regarding the two cultures comments, in particular “Type is where the theory-building is going on, and Prop is where the problem-solving is occurring”, this sounds odd from a propositions-are-some-types perspective. Isn’t the difference rather between situations where the type-formation is the more creative part (including conjecture or prop-formation) and situations where it’s rather the construction of an element of a type (or proof of a proposition) that’s trickiest?

    Like

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s