What is Lean?
Mathematical proofs have a strong egalitarian feature — in principle, anyone can check their validity, no matter who they are. It suffices to follow a chain of timeless logical reasoning, starting from given axioms. However, if you have ever tried to check all the steps in an advanced mathematical proof, you probably know that this is usually very far from truth in practice — the amount of work and prerequisite knowledge is enormous. That is why many mathematicians and computer scientists became interested in software proof assistants and formal verification tools (already in the 1960's!), such as HOL, Coq, Agda, Isabelle, and last but not least, Lean — which is the subject of this blog post series.
So, why choose Lean over the alternatives? After all, there is no "best approach" — all of these systems use different techniques and can inspire each other. Though Lean is well-suited to handle modern math, its main selling point is probably its very active community, which has exceeded a critical mass. One of the greatest feats is the impressive Mathlib library, which aims to unify as much of math as possible in a compatible and sufficiently general way. This opens the door for many mathematicians who might not have been interested otherwise. There are also other interesting projects, such as the Liquid Tensor Experiment — a successful formalization of a complex state-of-the-art result. This might not have been thinkable a couple years ago and it really feels like a new era for math. Adding artificial intelligence to the mix, we might witness interesting developments very soon. Imagine what we could do with all the intellectual capital freed up by not having to check hundreds of pages of technical proofs!
Why to get started
If becoming a pioneer in a potentially revolutionary area is not sufficient for you, here are some other compelling reasons:
- It's a lot of fun, almost like a video game! As the above screenshot of the interactive infoview shows, you can see the current hypotheses and goals at any given moment. You just need to find the right combination of commands to solve the puzzle, which can feel very satisfying.
- Sharpen your math thinking by clearly seeing the structure of your proofs. Even when you understand the topic well, you can gain new insights (e.g., which parts of the proof can be generalized to other contexts, how much information do different definitions carry,…). After all, teaching something is the best way to fully grasp it, and having an unforgiving and meticulous language as a student is perfect for this purpose.
- Participate in interesting interdisciplinary projects that might not have been accessible otherwise. E.g., even if you don't the required theoretical background, you can still work on the software engineering part, and vice versa.
- Can't choose between doing math and programming? No worries, you can now do both at the same time!
- Train your mental endurance through withstanding all the suffering caused by the incomplete documentation, lack of tutorials and live changes to the language. Seriously, this might be the weakest point of the Lean experience for beginners, so be prepared to face obstacles. (This is also the main reason for creating this series, focused mainly on tactic writing.) The good news is that the port of Mathlib from Lean 3 to Lean 4 has recently been finished, so things should get better soon. In the meantime, Zulip is the best place to ask questions.
How to get started
To play with Lean, a good entry point might be the Natural number game; you can also use the online Playground. But once you commit to become a little more serious, you should get a local installation. For a more specific example usage, you can follow the README of our project (more about it later).
If you're still with me, let's dive in and actually do something in the next blog post!
If you have any suggestions for improving this blog post, please let me know.