A template for blueprint-driven formalization projects in Lean.

Repository hosting the resources for the Lean demo session of my talk presented at the weekly research seminar on CHallenges in ANalysis and GEometry (CHANGE) at the University of Trento on February 11, 2025.

Formalising the Ring of Integers in Quadratic Fields in the Lean proof assistant.

A formalisation of James and Liebeck's Representations and Characters of Groups

This repository formalizes in Lean the Burkholder martingale transform inequality, including the construction of Burkholder’s majorant function and its application to sharp Lp estimates for real-valued martingales.

This Lean 4 project formalizes a mathematical structure BinaryTreeWithRootandTops, which models a rooted, ordered binary tree whose nodes are pairs of disjoint, nonempty, finite subsets of a finite set. This is closely related with maximal laminar families.

A Lean 4/mathlib project formalizing Schauder bases and unconditional Schauder bases for Banach spaces.

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.