pitmonticone
Informal Mathematics @UniTrento || Formal Mathematics at Harmonic || Formalising in @LeanProver || Developing in @JuliaLang and @Python.
University of TrentoTrento, Italy
Pinned Repositories
FLT
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
MultilayerGraphs.jl
A Julia package for the creation, manipulation and analysis of the structure, dynamics and functions of multilayer graphs.
mathlib4
The math library of Lean 4
leanblueprint
plasTeX plugin to build formalization blueprints.
EnergySystemModelling
Resources for the Energy System Modelling course by Tom Brown at Karlsruhe Institute of Technology (2020).
LeanProject
Template for blueprint-driven formalization projects in Lean.
pitmonticone
Profile repository of Pietro Monticone.
PlantDiseaseClassification
Dataset Analysis & CNN Models Optimization for Plant Disease Classification.
equational_theories
A project to map out the relations between different equational theories of Magmas.
pfr
Repository for formalization of the Polynomial Freiman Ruzsa conjecture (and related results)
pitmonticone's Repositories
pitmonticone/BET
Project for "Machine-Checked Mathematics" at the Lorentz Center
pitmonticone/aimo-progress-prize
pitmonticone/BirkhoffErgodicThm
A proof of Pointwise Birkhoff Ergodic Theorem in Lean
pitmonticone/BonnAnalysis
Repository hosting code and blueprint for the collaborative formalisation seminar in Analysis at the University of Bonn.
pitmonticone/InternLM-Math
pitmonticone/ML-Papers-Explained
Explanation to key concepts in ML
pitmonticone/modern-maths-game4
Modern Mathematics Game in Lean 4
pitmonticone/NewLeanProject
pitmonticone/Poly
A Lean4 Formalization of Polynomial Functors
pitmonticone/PutnamBench
An evaluation benchmark for undergraduate competition math in Lean4, Isabelle, Coq, and natural language.
pitmonticone/verbose-lean4
Natural language tactics to teach mathematics using Lean 4
pitmonticone/agda-unimath
The agda-unimath library
pitmonticone/batteries
The "batteries included" extended library for the Lean programming language and theorem prover
pitmonticone/Bayesian-Statistics
This repository holds slides and code for a full Bayesian statistics graduate course.
pitmonticone/carleson
[WIP] A formalised proof of a generalised Carleson's Theorem in the Lean proof assistant.
pitmonticone/cookbook
A collection of guides and examples for the Gemini API.
pitmonticone/FIMO
pitmonticone/Goedel_HF_Lean
Formalising Gödel's incompleteness in Lean using hereditarily finite set theory. It closely follows S. Swierczkowski. Finite Sets and Gödel’s Incompleteness Theorems. Dissertationes mathematicae. IM PAN, 2003. URL https://books.google.co.uk/books?id=5BQZAQAAIAAJ.
pitmonticone/HepLean
pitmonticone/lean-action
GitHub action for standard CI in Lean projects
pitmonticone/lean4game
pitmonticone/leanprover-community.github.io
Hosts the website for mathlib and other Lean community infrastructure.
pitmonticone/libro
Il grande libro di ItaCa
pitmonticone/ML-YouTube-Courses
📺 A place to discover the latest machine learning courses on YouTube.
pitmonticone/MMT
The MMT Language and System
pitmonticone/pymnet
The original library for analysing multilayer networks. https://mnets.github.io/pymnet/
pitmonticone/scientific-computing-lean
work in progress book on Scientific Computing in Lean
pitmonticone/snn-sound-localization
Training spiking neural networks for sound localization
pitmonticone/testing-lower-bounds
Lower bounds for hypothesis testing and estimation, in Lean
pitmonticone/uniformal.github.io
Main website for MMT and related material