Here are some useful links and references for our seminar:

Kevin Buzzard’s course repository: This will be the primary reference of our seminar.

Mathlib

The Informal Formalization Seminar in Utrecht

Theorem Proving in Lean: This reference is here because it gets into what is going on “under the hood” of lean.

Mathematics in Lean textbook

The Natural Numbers Game

Mir’s Masters Thesis: Explains how to formalize the notion of scheme (in Lean 3).

Buzzard’s Xena project: Contains many of the above links plus many more!