• LeanBlueprint: Python library to write blueprints for formalisation projects in the Lean proof assistant.
• LeanProject: Template for blueprint-driven formalization projects in Lean.
• Mathlib: Lean library of formalised mathematics.

• EquationalTheories: Mapping out and formalising the relations between different equational theories of magmas in the Lean proof assostant.

• BonnAnalysis: Collaborative formalisation seminars in Analysis at the University of Bonn.
• Carleson: Formalising a generalised Carleson's Theorem in the Lean proof assistant.

• FLT3: Formalising Fermat's Last Theorem for Exponent 3 in the Lean proof assistant.
• FLT: Formalising Fermat's Last Theorem in the Lean proof assistant.
• PFR: Formalising the Polynomial Freiman Ruzsa conjecture and related results in the Lean proof assistant.
• PNT+: Formalising the Prime Number Theorem and more in the Lean proof assistant.

• BET: Formalising Birkhoff's Ergodic Theorem in the Lean proof assistant.
• TopologicalEntropy: Formalising topological entropy in the Lean proof assistant and integrating it into Mathlib.

• HepLean: Formalising high energy physics in the Lean 4 proof assistant.

• When: 2025/02/11
• Where:University of Trento, Trento, Italy
• What: "An Invitation to Blueprint-Driven Formalisation of Mathematical Research in Lean" (Website,Slides,Demo)

• When: 2024/07/29 - 2024/08/02
• Where:Hausdorff Research Institute for Mathematics, Bonn, Germany
• What: "Getting Started with Blueprint-Driven Formalisation Projects in Lean" (Website,Video)

• When: 2023/05/23 - 2023/05/26
• Where:The Fields Institute, Toronto, Canada
• What: "Multilayer Network Science in Julia withMultilayerGraphs.jl" (Website,Slides,Video)

• When: 2023/07/25 - 2023/07/29
• Where:Massachusetts Institute of Technology, Cambridge, MA, USA
• What: "MultilayerGraphs.jl: Multilayer Network Science in Julia" (Website,Short Presentation,Long Presentation,Video)

PinnedLoading

1. leanprover-community/mathlib4leanprover-community/mathlib4Public

   The math library of Lean 4

   Lean 1.8k 387

2. PatrickMassot/leanblueprintPatrickMassot/leanblueprintPublic

   plasTeX plugin to build formalization blueprints.

   Python 189 33

3. teorth/equational_theoriesteorth/equational_theoriesPublic

   A project to map out the relations between different equational theories of Magmas.

   C 307 68

4. ImperialCollegeLondon/FLTImperialCollegeLondon/FLTPublic

   Ongoing Lean formalisation of the proof of Fermat's Last Theorem

   Lean 395 58

5. teorth/pfrteorth/pfrPublic

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

   Lean 147 36

6. JuliaGraphs/MultilayerGraphs.jlJuliaGraphs/MultilayerGraphs.jlPublic

   A Julia package for the creation, manipulation and analysis of the structure, dynamics and functions of multilayer graphs.

   Julia 122 4