This is the Lean 3 repo for Kevin Buzzard's 2022 EPSRC TCC course where he just does some experiments with algebraic geometry in Lean. The course consists of four 2-hour lectures (there were also four introductory lectures on more basic material, which are not included here).
There will also be an accompanying youtube video for each lecture.
Lecture 1) Sheaves of modules. Lecture 2) The sheaf of modules on Spec(R) attached to an R-module. Lecture 3) (to come) pushforwards.