LeanSearchClient
Syntax for searching with natural language from Lean, using https://leansearch.net/ (may extend to other services)
of 85 packages depending on leanprover-community/LeanSearchClient
1-20Sort by
Package Name
FR-vdash-bot/algorithmuses
d7caecc
Verified efficient algorithms in Lean4.jsm28/AMuses
d7caecc
Lean formalization of aperiodic monotiles papers (staging repository for material not yet in mathlib)dwrensha/animateuses
d7caecc
tool for turning Lean proofs into Blender animationsFormalizedFormalLogic/arithmetizationuses
d7caecc
Formalization of Arithmetization of Mathematics/Metamathematicsmseri/BETuses
7bedaed
Project for "Machine-Checked Mathematics" at the Lorentz Centersven-manthe/borel_detuses
d7caecc
jaalonso/Calculemus2uses
d7caecc
Proof exercises in Lean4 and Isabelle/HOLjaalonso/Calculemus2_esuses
d7caecc
Ejercicios de demostraciĆ³n con Lean4 e Isabelle/HOL.fpvandoorn/carlesonuses
d7caecc
A formalized proof of Carleson's theorem in Leandwrensha/Chessuses
d7caecc
Chess in Lean 4RemyDegenne/cltuses
2ba60fa
Central limit theorem in LeanGasStationManager/CodeProofTheArenauses
d7caecc
Lean coding problem solving challenge website with proof verificationdwrensha/compfilesuses
d7caecc
Catalog Of Math Problems Formalized In Leanleanprover-community/ConNFuses
d7caecc
A formal consistency proof of Quine's set theory New Foundationsteorth/equational_theoriesuses
d7caecc
A project to map out the relations between different equational theories of Magmas.MichaelStollBayreuth/EulerProductsuses
d7caecc
An attempt at formalizing facts on Euler products in Leangsierra99/ExFormMathL4uses
86d0d05
teorth/expdbuses
d7caecc
Exponent pair databaseImperialCollegeLondon/FLTuses
d7caecc
Ongoing Lean formalisation of the proof of Fermat's Last Theoremleanprover-community/flt-regularuses
d7caecc
Fermat's Last Theorem for regular primes