PI

Pietro Monticone

Informal Mathematics @UniTrento || Formal Mathematics at @Harmonic-AI || Formalising in @LeanProver || Developing in @JuliaLang and @Python.

Trento, Italy

Joined April 2018

1026 Followers

0 Following

AI Insights & Achievements

58/ 100

27 new projects with 29 stars.

54 day streak.

Coding for 8 years.

Profile README

GitHub Metrics

Current Selected Projects

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.

InfinityCosmos: Formalising the Infinity Cosmos theory 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.
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.

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.

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)

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 with MultilayerGraphs.jl" (Website, Slides, Video)