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 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.)
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!
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...
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.
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!
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...