Skip to content
View pitmonticone's full-sized avatar
953 followers · 0 following

Achievements

Achievement: Galaxy BrainAchievement: Pull Sharkx4Achievement: Pair Extraordinairex4Achievement: YOLOAchievement: QuickdrawAchievement: Public SponsorAchievement: StarstruckAchievement: Arctic Code Vault Contributor

Achievements

Achievement: Galaxy BrainAchievement: Pull Sharkx4Achievement: Pair Extraordinairex4Achievement: YOLOAchievement: QuickdrawAchievement: Public SponsorAchievement: StarstruckAchievement: Arctic Code Vault Contributor

Highlights

  • Pro

Organizations

@NVIDIAGameWorks @JuliaGraphs @JuliaDynamics @StatisticalRethinkingJulia @JuliaCommunity @InPhyT @JuliaHealth @DoriaLab @UniTo-SEPI @BayesianDataAnalysisJulia @NeuronalDynamicsJulia @JuliaEpi @JuliaTrustworthyAI @TidierOrg @FormalMathematicsLab

Block or report pitmonticone

Block user

Prevent this user from interacting with your repositories and sending you notifications. Learn more about blocking users.

You must be logged in to block users.

Maximum 250 characters. Please don't include any personal information such as legal names or email addresses. Markdown supported. This note will be visible to only you.
Report abuse

Contact GitHub support about this user’s behavior. Learn more about reporting abuse.

Report abuse
pitmonticone/README.md

Gmail Twitter GitHub Goodreads YouTube Mastodon Mastodon

GitHub Metrics

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.

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.

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.

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.

Mathematical Physics

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

Talks

2025

CHANGE Seminar

2024

Libraries of Digital Mathematics Workshop

2023

18th Workshop on Algorithms and Models for Web Graphs

JuliaCon 2023

Pinned Loading

  1. leanprover-community/mathlib4 leanprover-community/mathlib4 Public

    The math library of Lean 4

    Lean 2.5k 864

  2. PatrickMassot/leanblueprint PatrickMassot/leanblueprint Public

    plasTeX plugin to build formalization blueprints.

    Python 253 45

  3. teorth/equational_theories teorth/equational_theories Public

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

    Lean 439 89

  4. ImperialCollegeLondon/FLT ImperialCollegeLondon/FLT Public

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

    Lean 733 97

  5. teorth/pfr teorth/pfr Public

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

    Lean 192 41

  6. JuliaGraphs/MultilayerGraphs.jl JuliaGraphs/MultilayerGraphs.jl Public

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

    Julia 126 5