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!