Textbooks

In the course I plan to follow parts of the books Mathematics in Lean and Theorem Proving in Lean.

There is also Functional programming in Lean which might be useful as well.

Course repository

I’ve made (another) github repository for the course, to contain the Lean materials.

https://github.com/gmcninch-tufts/math190formalize

If you click that link, you’ll see instructions for using Gitpod to interact with course materials.

And you’ll see instructions for installing Lean on your computer.

Resources

• The definitive website for information on Lean is found here:

  LEAN-prover community

• introductory “games”

  There are some “learning games” available for Lean, including the natural numbers game.

  Playing through these games allows you to begin interacting with Lean.