blueprint for prime number theorem and more

Graphical rewriting for diagrammatic reasoning in monoidal categories in Lean4

plasTeX plugin to build formalization blueprints.

Repository for formalization of the Polynomial Freiman Ruzsa conjecture (and related results)

The math library of Lean 4

Welcome to The Filter Game! This is also our M2R project supervised by Prof. Kevin Buzzard at Imperial College London

Lean 3's obsolete mathematical components library: please use mathlib4

Lean mathzoo

Attracting mathematicians (others welcome too) with no experience in proof verification interested in HoTT and able to use Agda for HoTT

Tower of Hanoi in Lean!

A gamification of the theorems in MATH40002 Analysis 1

Source code for the Mathematics in Lean tutorial.

The user home repository for the Mathematics in Lean tutorial.

Condensed mathematics in Lean

Lean proof that a normed vector space with compact unit ball is finite dimensional

Formalising lecture notes from 1st year Imperial Mathematics course.

Group Cohomology