A template for blueprint-driven formalization projects in Lean.
Repository hosting resources for the "Lean Tutorial in Vienna" at TU Wien from September 18 to 20, 2024.
Course repository for GlaMS - Formalising Mathematics in Lean (2024)
(Attempt of) Formalising the GAGA theorem
Formalising non-commutative graph theory in Lean
Lean formalization of the Zhang Yeung inequality
Repository hosting resources for the 2024 workshop "Computer-Verified Proofs: 48 Hours in Rome" organised by @oliver-butterley, @RafaelGreenblatt and @marcolenci.
This Lean 4 project to formalize the main results on Besov spaces for measure spaces with good grids, as defined in Smania D. Besov-ish spaces through atomic decomposition. Analysis & PDE Vol. 15 (2022), No. 1, 123-174. We already formalized 90% of the paper.
This is a Lean 4 project whose goal is to formalize the construction of unbalanced Haar wavelets on measure spaces equipped with a finite measure and a sequence of finite measurable partitions.
Add a description, image, and links to the formalisation-mathematics topic page so that developers can more easily learn about it.
To associate your repository with the formalisation-mathematics topic, visit your repo's landing page and select "manage topics."