LeanSearchClient
Syntax for searching with natural language from Lean, using https://leansearch.net/ (may extend to other services)
of 165 packages depending on leanprover-community/LeanSearchClient
1-20Sort by
Package Name
b-mehta/ABCExceptionsuses
6c62474
Exceptions to the ABC conjecture in LeanYaelDillies/AddCombiuses
6c62474
The (currently unofficial) sublibrary of Mathlib dedicated to additive combinatoricslindy-labs/aegisuses
2507836
Verify Cairo contracts in Lean 4FR-vdash-bot/algorithmuses
8d29bc2
Verified efficient algorithms in Lean4.jsm28/AMuses
2507836
Lean formalization of aperiodic monotiles papers (staging repository for material not yet in mathlib)dwrensha/animateuses
8d29bc2
tool for turning Lean proofs into Blender animationsFormalizedFormalLogic/arithmetizationuses
0c169a0
Formalization of Arithmetization of Mathematics/MetamathematicsVerified-zkEVM/Arklibuses
6c62474
Formally Verified Arguments of Knowledge in Leaneshelyaron/bdduses
6c62474
Binary Decision Diagrams in Lean 4mseri/BETuses
7bedaed
Project for "Machine-Checked Mathematics" at the Lorentz Centerestradilua/BirkhoffErgodicThmuses
2507836
A proof of Pointwise Birkhoff Ergodic Theorem in Leanroos-j/BooleanFunuses
003ff45
Formalization project on analysis of Boolean functions in Lean 4, including a proof of Arrow's theorem via Fourier analysis.sven-manthe/borel_detuses
8d29bc2
RemyDegenne/BrownianMotionuses
6c62474
Construction of a Brownian Motion in Leanchrisflav/bruhat-titsuses
2507836
A formalisation of the Bruhat-Tits tree in Lean4RikHeurter/BscThesisFormalisationuses
2507836
jaalonso/Calculemus2uses
2507836
Proof exercises in Lean4 and Isabelle/HOLjaalonso/Calculemus2_esuses
003ff45
Ejercicios de demostración con Lean4 e Isabelle/HOL.fpvandoorn/carlesonuses
6c62474
A formalized proof of Carleson's theorem in Leanknowsys/certifyingDataloguses
6c62474
A certified checker for Datalog entailments, written in Lean