Highlights
- Pro
Stars
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)
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
Attracting mathematicians (others welcome too) with no experience in proof verification interested in HoTT and able to use Agda for HoTT
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.
Lean proof that a normed vector space with compact unit ball is finite dimensional
Formalising lecture notes from 1st year Imperial Mathematics course.