-
Notifications
You must be signed in to change notification settings - Fork 298
Where to start learning Lean
This zulip chat is where the Lean research community hangs out. There are lots of people there willing to answer basic questions from newcomers, and indeed are interested in figuring out the best answers to such questions. This page is an attempt to compile a community answer to one very frequent and important question: "I just finished introductory material X, what should I do next?" (where X is often the natural numbers game.)
- The zulip chat
- Play the natural number game
- Install Lean
- mathlib and the mathlib-docs
- Theorem Proving in Lean textbook
- Mathematics in Lean textbook
- Hitchhiker's guide to logical verification (pdf link)
- Logic and Proof
- lean-tutorials
- Codewars
- Learn you a Haskell for Great Good
This game/textbook/tutorial gets you from 0 to "writing nontrivial lean code" in just a few minutes, without any fussy software installation. Assuming you already know the math behind induction and the natural numbers, you'll formally prove many basic properties in just a few hours. If you're not so comfortable with the math, the Lean interpreter plus the Zulip chat make a good teacher :)
It has received positive reviews from a wide variety of players, including people who then don't go on to study Lean further. Every once in a while it goes viral on Reddit or HackerNews. The "engine" is open source, so anyone that can write Lean code and use github can produce "computer game levels" in the same format. (If you do, start a list for them right here?)
The above links give step-by-step instructions for installing the "leanproject" command-line tool, which can install Lean+mathlib and keep your installation up to date.
The instructions are a little fiddly; it can matter a lot to do the steps in order without mistakes.
For most people, it is much easier to follow these instruction than to install Lean on your own. Importantly, installing Lean on your own probably won't get you mathlib. Doing math in Lean without mathlib is like using OCaml without Base or doing machine learning in Python without tensorflow/pytorch. Also, the above instructions will get you the latest community version of Lean 3, which has some improvements over the last official release. (Development on Lean 3 at Microsoft has halted in favor of work on Lean 4.) Using the latest version of Lean+mathlib means having access to more power and user-friendly tactics. Perhaps most importantly, it means that if you ask for help in chat, people will be able to reproduce your errors exactly.
TPiL short for "Theorem Proving in Lean" is a good reference for stuff like "what's a Pi type?", "how do typeclasses work?", or "woah, you can define functions via pattern matching!?"
Hitchhiker's guide to logical verification (pdf link)
If the programming bits of Lean are hard for you, Learn you a Haskell for Great Good offers a gentler introduction to "functional programming", i.e. programming in a language where functions are data.
Codewars is a website for programming exercises. It has the quirk that exercises are called "kata" (and users are sometimes referred to as "codewarriors"). Codewars has over 50 Lean kata. Each kata requires you to write some Lean code to prove some specific theorem. (In principle you could also have Lean kata that are about writing tactics, but none exist as of May 8, 2020.) After you submit working code, you get to compare your solutions with other people's. It's a great way to find tricks that you didn't know you were missing.
Codewars also forces you to learn some things about how to make Lean code run more efficiently. For each kata, your entire solution needs to compile in less than 20 seconds on a computer which is ~3 times slower than Kevin Buzzard's home machine.
The kata marked "8 kyu" are suitable for someone who's played just the first few screens of the natural number game. Kata ranked "n kyu" for smaller n are harder.