Intuitive, type-safe expression quotations for Lean 4.
of 203 packages depending on leanprover-community/Qq
1-20Sort by
Package Name
TristanCacqueray/advent-of-leanuses
d3a1d25
lindy-labs/aegisuses
v4.19.0-rc2
Verify Cairo contracts in Lean 4FR-vdash-bot/algorithmuses
v4.19.0-rc2
Verified efficient algorithms in Lean4.jsm28/AMuses
v4.20.0-rc2
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
v4.17.0-rc1
Formalization of Arithmetization of Mathematics/MetamathematicsVerified-zkEVM/Arklibuses
v4.18.0
Formally Verified Arguments of Knowledge in LeanBergschaf/banach_tarskiuses
01ad339
mseri/BETuses
1357f4f
Project for "Machine-Checked Mathematics" at the Lorentz Centerfpvandoorn/bonnAnalysisuses
a7bfa63
repository for the collaborative formalization seminar in Analysis in Bonnsven-manthe/borel_detuses
v4.19.0-rc2
RemyDegenne/BrownianMotionuses
v4.20.0-rc2
Construction of a Brownian Motion in Leanchrisflav/bruhat-titsuses
v4.19.0
A formalisation of the Bruhat-Tits tree in Lean4RikHeurter/BscThesisFormalisationuses
v4.19.0-rc2
jaalonso/Calculemus2uses
v4.20.0-rc2
Proof exercises in Lean4 and Isabelle/HOLjaalonso/Calculemus2_esuses
v4.14.0
Ejercicios de demostración con Lean4 e Isabelle/HOL.fpvandoorn/carlesonuses
v4.20.0-rc2
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
v4.17.0-rc1
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.