This semester (Fall 2026), we’ll run a seminar on Formalization of Math and Lean in the math department here at Tufts University.
Schedule: meets weekly in JCC 302, Tuesday 3:00-4:00.
seminar git repository
https://github.com/gmcninch-prof/tufts-lean-seminar/
Weekly info
| Week | meeting date | materials | follow-up remarks |
|---|---|---|---|
| 1 | 2026-09-15 | slides | remarks |
| 2 | 2026-09-22 | slides | remarks |
| 3 | 2026-09-29 |
The remarks should contain some suggested reading for the subsequent meeting.
References
The Lean prover community website has lots of Lean resources.
In particular, probably the first thing you need to know is how to install Lean on your computer. Note that you really do need to carry out all the steps in this installation process to have a working copy of Lean on your computer.
Before installation, you might try using this online version of Lean.
There is also a useful page of Learning resources
Two particularly useful “book-references” are
A good starting point for lean is the natural numbers game.
Here are some materials from Tufts graduate student Xiao Tan about programming and software verification in Lean.
I plan to post some notes for the seminar here.