Current Selected Projects

Libraries & Templates

• 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.
• PhysLib: Formalising high energy physics in the Lean 4 proof assistant.

Algebra

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

Analysis

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

Category Theory

• InfinityCosmos: Formalising the Infinity Cosmos theory in the Lean proof assistant.

Dynamical Systems Theory

• 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.

Number Theory

• 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.
• ABC-Exceptions: Formalising the exceptional set in the ABC conjecture in the Lean proof assistant.
• SpherePacking: Formalising Maryna Viazovska's Fields Medal-winning solution to the sphere packing problem in dimension 8.

Open Problems

• ErdosProblems: Solving and formalising Erdös problems with Aristotle in the Lean proof assistant.

Talks

2025

ItaLean 2025

• When: 2025/12/09 - 2025/12/12
• Where: University of Bologna, Bologna, Italy
• What: "LeanArchitect: Automating Blueprint Generation for Humans and AI" (Website, Slides, GitHub, Video)

CHANGE Seminar

• 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)

2024

Libraries of Digital Mathematics Workshop

• 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)

2023

18th Workshop on Algorithms and Models for Web Graphs

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

JuliaCon 2023

• 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)