LeanSearchClient
Syntax for searching with natural language from Lean, using https://leansearch.net/ (may extend to other services)
1-20 of 93 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
d7caeccLean formalization of aperiodic monotiles papers (staging repository for material not yet in mathlib)dwrensha/animateuses
d7caecctool for turning Lean proofs into Blender animationsFormalizedFormalLogic/arithmetizationuses
003ff45Formalization of Arithmetization of Mathematics/Metamathematicsmseri/BETuses
7bedaedProject for "Machine-Checked Mathematics" at the Lorentz Centersven-manthe/borel_detuses
d7caeccjaalonso/Calculemus2uses
d7caeccProof exercises in Lean4 and Isabelle/HOLjaalonso/Calculemus2_esuses
003ff45Ejercicios de demostración con Lean4 e Isabelle/HOL.fpvandoorn/carlesonuses
d7caeccA formalized proof of Carleson's theorem in Leandwrensha/Chessuses
d7caeccChess in Lean 4RemyDegenne/cltuses
2ba60faCentral limit theorem in LeanGasStationManager/CodeProofTheArenauses
d7caeccLean coding problem solving challenge website with proof verificationdwrensha/compfilesuses
003ff45Catalog Of Math Problems Formalized In Leanleanprover-community/ConNFuses
d7caeccA formal consistency proof of Quine's set theory New Foundationsteorth/equational_theoriesuses
d7caeccA project to map out the relations between different equational theories of Magmas.MichaelStollBayreuth/EulerProductsuses
d7caeccAn attempt at formalizing facts on Euler products in Leangsierra99/ExFormMathL4uses
d7caeccteorth/expdbuses
003ff45Exponent pair databaseImperialCollegeLondon/FLTuses
003ff45Ongoing Lean formalisation of the proof of Fermat's Last Theorem