plausiblev0.1.0
of 152 packages depending on leanprover-community/plausible
1-20Sort by
Package Name
b-mehta/ABCExceptionsuses
v4.21.0-rc3
Exceptions to the ABC conjecture in LeanYaelDillies/AddCombiuses
v4.20.0
The (currently unofficial) sublibrary of Mathlib dedicated to additive combinatoricslindy-labs/aegisuses
v4.20.0-rc2
Verify Cairo contracts in Lean 4FR-vdash-bot/algorithmuses
4dfba8b
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-rc1
tool for turning Lean proofs into Blender animationsFormalizedFormalLogic/arithmetizationuses
v4.17.0-rc1
Formalization of Arithmetization of Mathematics/MetamathematicsVerified-zkEVM/Arklibuses
v4.21.0-rc3
Formally Verified Arguments of Knowledge in Leaneshelyaron/bdduses
v4.20.0-rc2
Binary Decision Diagrams in Lean 4estradilua/BirkhoffErgodicThmuses
v4.20.0-rc2
A proof of Pointwise Birkhoff Ergodic Theorem in Leanroos-j/BooleanFunuses
v4.16.0-rc1
Formalization project on analysis of Boolean functions in Lean 4, including a proof of Arrow's theorem via Fourier analysis.sven-manthe/borel_detuses
v4.19.0-rc2
RemyDegenne/BrownianMotionuses
v4.21.0-rc3
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.15.0-rc1
Ejercicios de demostración con Lean4 e Isabelle/HOL.fpvandoorn/carlesonuses
v4.21.0-rc3
A formalized proof of Carleson's theorem in Leanknowsys/certifyingDataloguses
v4.20.0
A certified checker for Datalog entailments, written in LeanYaelDillies/ChandraFurstLiptonuses
v4.20.0
Formalisation in the Lean theorem prover of the relation between corner-free sets and communication complexity