The semester has been rather quiet at ForAlli, but exciting things are going on in formalization of mathematics elsewhere! Let me highlight some recent items.
A milestone was reached in August that has enormous practical impact for Lean users: the porting of more than a million lines of Mathlib code from Lean3 to Lean4 was completed. The transition to Lean4 immediately brought many concrete improvements, but also with the existence of a stable system, new tools have since then started appearing at a fast pace. Most importantly, after a long wait there now is again a good choice of a language and a library of formalized math, so one can just go ahead and play!
Since the Liquid Tensor Experiment, there had not been other high-profile formalized mathematics projects of comparable impact. But in October, Terence Tao started a first "small" Lean project of formalizing a result of his, and after successfully completing it, Tao started a collaborative project of formalizing a recent result of Gowers, Green, Manners, and himself. This is mainstream mathematics (a proof of a major combinatorial result using largely probabilistic techniques), with two Fields medalists as authors, so the fact that its formalization is feasible is a serious indication about the seriousness of Lean as a proof assistant for formalizing serious mathematics. Already during his first smaller project, Tao made numerous comments about the formalization experience from a traditional mathematicians' point of view, and in his blog post about the new project he emphasized the collaborative aspects that formalization enables as well as the tools for structuring of such a project. Tao's writings are well worth reading. And now, given that Tao's collaborative project will be completed within a time span of just a few weeks, and given that there are now several other Fields medalists involved in various aspects of formalization of high-level mathematics, I think it is becoming evident that computer proof assistants will play a role in mathematics research in the future.
Let me end with a piece of news from closer to home. The Finnish Mathematical Society relaunched its colloquium in a new online format. The Fall 2023 colloquium, the first of the new kind, was given by Heather Macbeth on "Making mathematics computer checkable". Heather's talk is also aimed at a general mathematics audience, and she packs a remarkable amount of insight into her talk, often in the form of concrete examples. The recording of the talk is available on the Finnish Mathematical Society YouTube channel. Enjoy!
After a delay of the launch of the weekly meetings of ForAlli, we finally have the first live meeting today: Thursday, March 3, at 4pm, in the Top Lounge (U523, Otakaari 1, 5th floor).
The idea is that everyone can choose their own preferred activities, but coming together weekly we can discuss them and help each other. I expect that many are not yet familiar with formalization at all, so I list below a few suggestions of what to do first (and second), with some comments on the suitable background for each. You can delve in them on your own, or try them collaboratively with a friend — and you can in any case ask others and help others. Note that I have not gone through all of the listed resources myself, so it is not a bad idea to ask around whether others have tried them and how they felt about them. If you consider something below wildly inaccurate, let me know and I will try to correct it.
The Natural Number Game
The most straightforward starting point is the Natural Number Game (NNG). It does not require installing Lean, and it also doesn't require (almost) any mathematical background; the topic is just basic arithmetic properties of natural numbers. The catch is that in the game you prove those properties totally from scratch! You start from a construction (basically the Peano axioms) of the natural numbers, then define addition and multiplication of natural numbers from that foundational starting point, and there are a lot of puzzles to be solved before you even get the commutativity or associativity of those operations. The game introduces basics of Lean while you progress through the levels. It also corresponds fairly well to how formalization feels when you are building something entirely new from scratch. And, I should add, the narrative is impeccable!
(Sometimes the server is down, in which case you can play the NNG also via this mirror.)
Formalisation of Mathematics course
Kevin Buzzard has taught courses titled Formalisation of Mathematics at Imperial College London in 2021 and 2022. These can be quite good starting points for someone who already has the sufficient mathematical background (for example for a doctoral student of math). These courses do require you to have some form of working installation of Lean (installation instructions are linked, though). They focus on different mathematical topics for each "week", and let you do exercises about them. The idea is still to pick the basics of Lean along the way; no prior formalization experience is required. Compared to the Natural Number Game, the biggest difference is that this jumps directly to real university level math (topics from BSc and MSc level math courses, say). For this reason the courses use mathlib, Lean's mathematical library (currently more than 700000 lines of code and rapidly expanding). You gradually get familiar with parts of the library in the process. If you are interested in formalization of mathematics in Lean, this is a necessary step at some point anyway — you will not want to build absolutely everything from the ground up as in the Natural Number Game!
Introduction to University Mathematics course
Another course by Kevin Buzzard! This should be more accessible to, say, first year university students. But I haven't actually tried, so I'll instead be hoping for someone to tell me...
The tutorials project
An installation of Lean/mathlib basically comes with a tutorials project with it. The tutorials are collections of mathematical exercises in Lean, also using mathlib. The mathematical prerequisites include only some undergraduate topics. This is a very appropriate starting point (or a good continuation from the NNG), but with perhaps slightly less developed interface and supporting material than Buzzard's courses.
Lean for the Curious Mathematician
A workshop was organized in 2020, with the purpose of introducing formalization and Lean to mathematicians of various levels. The workshop was split to many different topics, introduced by different active mathlib contributors. The main content is exercises, supported with introductory YouTube videos for each topic. This certainly contains excellent material, but may be slightly outdated, since Lean's mathlib has developed very fast during the past two years.
Find resources by yourself
The above are just some resources I have come across with. You can find plently of others, if you think they are more suitable for you!
DIY!
Finally, you can of course just start formalizing your own favorite piece of math! This requires somehow getting familiar with the language and syntax first — the earlier suggestions may therefore still be relevant. A textbook about the language is the online book Theorem Proving in Lean. This is an exciting option, and we are all on our way there, but be warned! It is not going to be easy, formalization of mathematics is genuinely challenging! (And fun! Yes, that is also a warning.)
You may have noted that I am listing only Lean resources. There exist many other formalization languages, each with their own advantages. You are very welcome to choose your preferred one, but I will not be able to help at all with anything except possibly Lean — not even in suggesting learning resources...
We are launching FORALLI, short for the Formalization Alliance. Our main activity will be weekly meetings at Aalto University on Thursdays at 4pm starting in the Spring semester 2022. Everyone is welcome to write their own formalized proofs, help others write their formalized proofs, ask for help, discuss proofs (formalized or not), play proof games, or anything in this general ballpark. Our aim is to
- have fun
- learn some.
Besides the weekly meetings, we have this web page and this very blog, and an online chat forum: https://foralli.zulip.cs.aalto.fi.
If you are interested but don't know where to start, come to the meetings or ask on the Zulip. We will suggest ideas of what to do depending on your background and interests. Typically, we would recommend starting by playing the Natural Number Game --- a web-based puzzle game where the goals of the various levels are to prove some basic arithmetic properties of the natural numbers from scratch, i.e., directly from a construction of the natural number system (essentially the Peano axioms). The game is
- fun
- instructive about mathematical proofs in general and a good introduction to a formalization language called Lean.
Why formalize mathematics?
The most obvious advantage of formalized and computer verified proofs is a guarantee of their correctness. By its very nature, mathematics concerns itself with universal truths, and computer verification is the ultimate standard of rigor in checking that a given piece of mathematics does not contain any mistakes. The history of science knows numerous examples about mistakes in mathematics, and some of them make for truly fascinating stories that would be exciting to delve into... There are even ongoing disputes about the correctness of some proposed proofs for very high profile mathematical claims. One can imagine a world in which such disputes were settled once and for all by formal verification (it is important to add, however, that this is not feasible in reality, because formal verification is genuinely hard!). Moving away from unintentional mistakes, one can entertain scenarios in which a bad actor would deliberately try to be misleading, or even to cheat about math. I challenge you to put your conspiratorial creativity to a test by imagining how this could be done for the purpose of passing an exam, of advancing one's academic career, of obtaining unauthorized access to data, or of manipulating e.g. financial markets or blockchains. Whether we worry about accidental mistakes or deliberate abuse, with formal verification of each and every step of the underlying logic, we clearly gain trust.
But it is also important to understand that correctness guarantees are not the most compelling reasons to formalize mathematics; not to most of us, anyway --- they are merely the most evident one. I hope this blog will grow to have plenty of subsequent posts addressing various aspects of both how and why we do formalization of mathematics. You may want to check out Kevin Buzzard's invitation to formalization for mathematicians, to be presented at the International Congress of Mathematicians 2022. For now, I will just borrow a bullet point list from a talk by Jason Rute to briefly address the "why"-question (the talk was actually about a machine learning problem related to theorem proving, but this list was too good not to borrow). His answers to "Why formal theorem proving?" were the following:
- mechanically check mathematical proofs
- digitize mathematics
- unify and archive mathematical knowledge
- prove correctness of software and hardware
- make mathematics accessible to computers in a new way.
Every item above would deserve a discussion of its own (machine learning in particular pertains mostly to the last one). But it is worth noting that correctness is just one among the five points.
I find the list exquisitely well thought through and balanced. I only regret one serious omission in it. It forgets to mention that formalization of mathematics is fun! Whether you enjoy programming, puzzle games, philosophical foundations, or mathematics per se, the spirit of each is strongly present in formalization. Join us and have fun!