-
University of Trento
- Trento, Italy
- @PietroMonticone
- @[email protected]
- @PietroMonticone
Highlights
- Pro
-
EquationalTheories Public
Forked from teorth/equational_theoriesA project to map out the relations between different equational theories of Magmas.
-
pitmonticone Public
Profile repository of Pietro Monticone.
-
leanblueprint Public
Forked from PatrickMassot/leanblueprintplasTeX plugin to build formalization blueprints.
Python Apache License 2.0 UpdatedJan 24, 2025 -
LeanProject Public template
Template for blueprint-driven formalization projects in Lean.
-
FormalBook Public
Forked from mo271/FormalBookFormalizing "Proofs from THE BOOK"
-
psymple Public
Forked from casasglobal-org/psymplePython GNU General Public License v3.0 UpdatedJan 22, 2025 -
formalized-mathematics-in-lean Public
Forked from andrejbauer/formalized-mathematics-in-leanA graduate course on formalized mathematics at the Faculty of Mathematics and Physics, University of Ljubljana, Fall semester 2024/25
-
sphere-eversion Public
Forked from leanprover-community/sphere-eversionFormalization of the existence of sphere eversions
-
M2Lyon2425 Public
Forked from faenuccio-teaching/M2Lyon2425This is the repository for the Lean master program in Lyon for 2024-25
-
mathematics_in_lean_source Public
Forked from avigad/mathematics_in_lean_sourceSource code for the Mathematics in Lean tutorial.
Lean UpdatedJan 16, 2025 -
formalising-mathematics-notes Public
Forked from b-mehta/formalising-mathematics-notesCourse notes for Formalising Mathematics 2025
-
LeanInVienna2024 Public
Repository hosting resources for the "Lean Tutorial in Vienna" at TU Wien from September 18 to 20, 2024.
-
lean-update Public
Forked from oliver-butterley/lean-updateThe action attempts to update Lean and Mathlib. If an update is available then the updated version is tested. This allows for automatic committing of the updated project, opening PRs or opening iss…
-
verbose-lean4 Public
Forked from PatrickMassot/verbose-lean4Natural language tactics to teach mathematics using Lean 4
-
-
LeanManual Public
Forked from leanprover/reference-manualJavaScript Apache License 2.0 UpdatedDec 17, 2024 -
seirmo Public
Forked from SABS-R3-Epidemiology/seirmoThis is a project to model the outbreak of an infectious disease with the SEIR model.
Python BSD 3-Clause "New" or "Revised" License UpdatedDec 13, 2024 -
Poly Public
Forked from sinhp/PolyA Lean4 Formalization of Polynomial Functors
-
lean4checker Public
Forked from leanprover/lean4checkerReplay the `Environment` for a given Lean module, ensuring that all declarations are accepted by the kernel.
-
checkdecls Public
Forked from PatrickMassot/checkdeclsTiny Lean library to check existence of declarations
Lean UpdatedNov 30, 2024 -
-
mahler Public
Forked from giuliocaflisch/mahlerCode in Lean 4 for my Bachelor Thesis.
-
-
doc-gen4 Public
Forked from leanprover/doc-gen4Document Generator for Lean 4
-
PNT Public
Forked from AlexKontorovich/PrimeNumberTheoremAndblueprint for prime number theorem and more
Lean Apache License 2.0 UpdatedNov 13, 2024 -
GlimpseOfLean Public
Forked from PatrickMassot/GlimpseOfLeanAn introduction to theorem proving in Lean for the impatient.
Lean Apache License 2.0 UpdatedNov 8, 2024 -
crypto Public
Forked from boazbk/cryptoLecture notes for a course on cryptography
TeX Other UpdatedNov 7, 2024 -
LeanCourse24 Public
Forked from fpvandoorn/LeanCourse24Bonn Lean course for winter 24/25
-
hoi Public
Forked from brainets/hoiHigher-Order Interactions
Python BSD 3-Clause "New" or "Revised" License UpdatedOct 30, 2024 -
ImProver Public
Forked from riyazahuja/ImProverImProver: Agent-Based Automated Proof Optimization