LeanSearchClient
Syntax for searching with natural language from Lean, using https://leansearch.net/ (may extend to other services)
1-20 of 118 packages depending on leanprover-community/LeanSearchClient
Sort by
Package Name
lindy-labs/aegisuses
d7caeccVerify Cairo contracts in Lean 4FR-vdash-bot/algorithmuses
d7caeccVerified efficient algorithms in Lean4.jsm28/AMuses
ba020edLean formalization of aperiodic monotiles papers (staging repository for material not yet in mathlib)dwrensha/animateuses
003ff45tool for turning Lean proofs into Blender animationsFormalizedFormalLogic/arithmetizationuses
0c169a0Formalization of Arithmetization of Mathematics/Metamathematicsmseri/BETuses
7bedaedProject for "Machine-Checked Mathematics" at the Lorentz Centersven-manthe/borel_detuses
003ff45jaalonso/Calculemus2uses
d7caeccProof exercises in Lean4 and Isabelle/HOLjaalonso/Calculemus2_esuses
003ff45Ejercicios de demostración con Lean4 e Isabelle/HOL.fpvandoorn/carlesonuses
ba020edA formalized proof of Carleson's theorem in Leanknowsys/certifyingDataloguses
0c169a0A certified checker for Datalog entailments, written in LeanYaelDillies/ChandraFurstLiptonuses
0c169a0Formalisation in the Lean theorem prover of the relation between corner-free sets and communication complexitydwrensha/Chessuses
003ff45Chess in Lean 4RemyDegenne/cltuses
ba020edCentral limit theorem in LeanGasStationManager/CodeProofTheArenauses
d7caeccLean coding problem solving challenge website with proof verificationvihdzp/combinatorial-gamesuses
0c169a0Combinatorial game library in Lean 4dwrensha/compfilesuses
ba020edCatalog Of Math Problems Formalized In LeanTimeroot/computableRealuses
003ff45computable implementation of real numbers in Lean4leanprover-community/ConNFuses
0c169a0A formal consistency proof of Quine's set theory New FoundationsVCA-EPFL/dataflow-rewriteruses
d7caecc