The Sphere Eversion Project

The perfectoid project.

Johan Commelin and I worked with Patrick Massot on the Lean perfectoid space project, but Patrick is not an algebraic number theorist, and he found our literature hard to read in places. He was constantly picking up on what I would regard as “typos” or “obvious slips” in Wedhorn’s unpublished (and at that time unavailable) notes — stuff which was throwing him off. Wedhorn’s notes contain an explicit warning on the front that they are not finished and you read them at your own risk, but Johan and I were between us expert enough to be able to explain precisely what was going on whenever Patrick asked about operator precedence or the meaning of some undefined \cdot . Torsten Wedhorn — thank you for your blueprint, now finally available on ArXiv . We learnt a lot from it — both about the definition of an adic space, and about how to write blueprints.

The point Patrick wanted me to understand was this: If I as a mathematician thought I really knew the definition of a perfectoid space, why couldn’t I come up with a precise and error-free and furthermore self-contained mathematical document that he, as a non-expert but as a professional mathematician, would be able to read without difficulty? Where was my plan for formalising perfectoid spaces? The answer to that was that the plan was in my head. Along the way, Patrick in particular learnt that there are problems with this approach.

The cap set problem.

In stark contrast to the perfectoid shambles was work of Sander R. Dahmen, Johannes Hölzl, Robert Y. Lewis on the Cap Set Problem — see their ArXiv paper. Their main result is a complete computer proof formalisation of the main theorem in the 2017 Annals of Mathematics paper by Ellenberg and Gijswijt on the cap set problem. Sander, Johannes and Rob organised their workflow very differently. They started with a detailed pdf document written by Dahmen (a mathematician). This old-fashioned proof was self-contained, just did normal maths in a normal way, and didn’t mention Lean once. It is a document which will convince any proper mathematician who cares to read it carefully of the correctness of the proof. Dahmen’s work is a completely rigorous old-fashioned proof of the theorem. There is no doubting its correctness. But because it is complete, correct, and self-contained modulo undergraduate level mathematics, this means that people who are not necessarily specialists in mathematics can now begin to work together, using a computer system which knows a lot of undergraduate mathematics, and they can turn Dahmen’s blueprint into a proof of Ellenberg-Gijswijt stored as a virtual mathematical object in the memory of a computer. Such an object is far more amenable to AI analysis than the corresponding pdf file, because computers have a hard time reading natural language, even if written by mathematicians. Apparently we don’t always explain things correctly.

My point here is: Dahmen’s blueprint was an important part of the process.

The sphere eversion project.

But back to Patrick. He is conjecturing that Lean 3 is sufficiently powerful to formalise a complete proof of Sphere Eversion, the Proposition that you can turn a sphere inside-out without creasing it, as long as it is made out of material which has self-intersection 0, like light but bendier. There’s a video. 3D geometry is involved.

The amazing news is that Patrick has now written a blueprint for the proof. This is a normal mathematical document containing a proof of sphere eversion which anyone who knows enough maths to know what a manifold is, could check and see was a completely rigorous and self-contained proof. It is written by an expert in the area, and typeset in a clever way so it displays beautifully in a browser. It is an interactive blueprint. It is the beginning. It is half of the Rosetta Stone that Patrick is creating, which will explain one story in two languages — a human language, and a computer language.

Patrick has also started a Lean sphere eversion project on GitHub . This is a currently mostly empty Lean repository, which will ultimately contain a formal proof of sphere eversion if the project is successful.

Those two parts together form Patrick’s Sphere Eversion Project.

At some point in the near future, Patrick is going to need mathematicians to formalise parts of the proof. The people he’s looking for are perhaps people with degrees in mathematics who are interested in trying something new. Patrick and I, together with Rob Lewis and Jeremy Avigad, are still working hard on our forthcoming book Mathematics in Lean, an introduction to the skills that a mathematician will need in order to participate. Once you have learned how to write Lean, Patrick has some computer game puzzles which you might be interested in playing.

If anyone has questions, they could ask in the sphere eversion topic in #maths in the Zulip chat (login required, real names preferred, be nice), a focussed and on-topic Lean chat where many experts hang out. People who are looking for a less formal setting are welcome to join the Xena Discord server (meetings Thursday evening at 5ish).

The schemes project

What is so amazing about projects like these is that they are teaching us how to use dependent type theory as a foundation for all of pure mathematics. We have had occasional problems along the way. Every division ring is a ring and hence a monoid and thus a semigroup. Invisible functions piled up in type class inference. The perfectoid project helped guide us to the realisation that type class inference was becoming problematic at scales which mathematicians needed it to work, and the Lean developers have responded to this issue by completely redesigning the system in Lean 4.

But let me finish with my Lean schemes project — my first serious Lean project, written with Chris Hughes and Kenny Lau, both at the time first year undergraduates. The project is completely incompatible with modern Lean and mathlib, but if you compile it then you get a sorry-free proof that an affine scheme is a scheme. During our proof we ran into a huge problem because our blueprint, the Stacks Project, assumed that , and this turns out to be unprovable for Lean’s version of equality: this equality is in fact one of Milne’s “canonical” isomorphisms. The Lean community wrestled with this idea, and has ultimately come up with a beefed-up notion of equality for which the identity is now true. Amelia Livingston is just putting the finishing touches on its implementation in Lean — many thanks indeed Amelia. It has been an extraordinary journey, and one which has taught me a great deal about localisation and how to think about it. I had never realised before that the rationals might not be equal to the field of fractions of the integers — whether those two fields are actually equal is an implementation issue of no relevance to mathematicians. What we need to know is merely that they are isomorphic and that there is a preferred isomorphism in each direction. This has design consequences which we are only just beginning to understand properly.

I wish the sphere eversion project every success. I am confident that it will teach us more about how to formalise mathematics in dependent type theory.

Advertisement