Kevin Buzzard's Projects
Source for the community blog
Lean proof that a normed vector space with compact unit ball is finite dimensional
A Lean version manager
Experiments with definition of etale morphisms etc
Proof in Lean of Fermat Last Theorem for exponent 3
Some material for Lean 4 lectures at IISc
My personal GitHub repo
Lean Theorem Prover
This project converts structured Lean code into an interactive browser game.
A skeleton repo for use with the Lean game maker
144 is the largest square in the Fibonacci sequence
Formal verification of parts of the Stacks Project in Lean
thinking about a "filter game" in Lean 4.
plasTeX plugin to build formalization blueprints.
Hosts the website for mathlib and other Lean community infrastructure.
www
Learning material for mathematicians who want to learn Lean
Lean mathematical components library
Development tools for https://github.com/leanprover-community/mathlib
Porting random files from Lean 3 mathlib into Lean 4, just for fun.
Mathport is a tool for porting Lean3 projects to Lean4
An abstraction of a maze.
Mathlib4 hierarchy skeletons for making mathlib-free MWEs in Lean 4
Natural Number Game
Defining numbers as equivalence classes of finite types
Benchmark for undergraduate-level formal mathematics