mathlib
The math library of Lean 4
of 221 packages depending on leanprover-community/mathlib
1-20Sort by
Package Name
TristanCacqueray/advent-of-leanuses
v4.3.0
lindy-labs/aegisuses
v4.19.0-rc3
Verify Cairo contracts in Lean 4FR-vdash-bot/algorithmuses
v4.19.0-rc2
Verified efficient algorithms in Lean4.jsm28/AMuses
01239f4
Lean formalization of aperiodic monotiles papers (staging repository for material not yet in mathlib)dwrensha/animateuses
v4.18.0
tool for turning Lean proofs into Blender animationsFormalizedFormalLogic/arithmetizationuses
f05ed67
Formalization of Arithmetization of Mathematics/MetamathematicsVerified-zkEVM/Arklibuses
v4.18.0
Formally Verified Arguments of Knowledge in LeanBergschaf/banach_tarskiuses
15ce681
mseri/BETuses
0a0178f
Project for "Machine-Checked Mathematics" at the Lorentz Centerfpvandoorn/bonnAnalysisuses
b387c54
repository for the collaborative formalization seminar in Analysis in Bonnsven-manthe/borel_detuses
32a0a63
RemyDegenne/BrownianMotionuses
b375a6d
Construction of a Brownian Motion in Leanchrisflav/bruhat-titsuses
v4.19.0
A formalisation of the Bruhat-Tits tree in Lean4RikHeurter/BscThesisFormalisationuses
f8ab294
jaalonso/Calculemus2uses
eb25653
Proof exercises in Lean4 and Isabelle/HOLjaalonso/Calculemus2_esuses
a8f082c
Ejercicios de demostración con Lean4 e Isabelle/HOL.fpvandoorn/carlesonuses
a336c58
A formalized proof of Carleson's theorem in Leanknowsys/certifyingDataloguses
v4.17.0
A certified checker for Datalog entailments, written in LeanYaelDillies/ChandraFurstLiptonuses
v4.19.0
Formalisation in the Lean theorem prover of the relation between corner-free sets and communication complexitypitmonticone/CHANGEuses
c1d4716
Repository hosting the resources for the Lean demo session of my talk presented at the weekly research seminar on CHallenges in ANalysis and GEometry (CHANGE) at the University of Trento on February 11, 2025.