A template for blueprint-driven formalization projects in Lean.
-
Updated
Jan 26, 2026 - Python
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.
A formalisation of James and Liebeck's Representations and Characters of Groups
Formalising the Ring of Integers in Quadratic Fields in the Lean proof assistant.
Add a description, image, and links to the formalised-mathematics topic page so that developers can more easily learn about it.
To associate your repository with the formalised-mathematics topic, visit your repo's landing page and select "manage topics."