No results found

LeanSearchClient

Syntax for searching with natural language from Lean, using https://leansearch.net/ (may extend to other services)
Displaying 1-20 of 129 packages depending on leanprover-community/LeanSearchClient
Sort by

  1. lindy-labs/aegisuses2507836

    Verify Cairo contracts in Lean 4

  2. FR-vdash-bot/algorithmuses8d29bc2

    Verified efficient algorithms in Lean4.

  3. jsm28/AMuses8d29bc2

    Lean formalization of aperiodic monotiles papers (staging repository for material not yet in mathlib)

  4. dwrensha/animateuses0c169a0

    tool for turning Lean proofs into Blender animations

  5. FormalizedFormalLogic/arithmetizationuses0c169a0

    Formalization of Arithmetization of Mathematics/Metamathematics

  6. Verified-zkEVM/Arklibuses8d29bc2

    Formally Verified Arguments of Knowledge in Lean

  7. mseri/BETuses7bedaed

    Project for "Machine-Checked Mathematics" at the Lorentz Center

  8. sven-manthe/borel_detuses8d29bc2

  9. jaalonso/Calculemus2uses2507836

    Proof exercises in Lean4 and Isabelle/HOL

  10. jaalonso/Calculemus2_esuses003ff45

    Ejercicios de demostración con Lean4 e Isabelle/HOL.

  11. fpvandoorn/carlesonuses2507836

    A formalized proof of Carleson's theorem in Lean

  12. knowsys/certifyingDataloguses0c169a0

    A certified checker for Datalog entailments, written in Lean

  13. YaelDillies/ChandraFurstLiptonuses8d29bc2

    Formalisation in the Lean theorem prover of the relation between corner-free sets and communication complexity

  14. dwrensha/Chessuses003ff45

    Chess in Lean 4

  15. Verified-zkEVM/Cleanuses0c169a0

    Lean circuit DSL

  16. RemyDegenne/cltuses2507836

    Central limit theorem in Lean

  17. GasStationManager/CodeProofTheArenausesd7caecc

    Lean coding problem solving challenge website with proof verification

  18. vihdzp/combinatorial-gamesuses0c169a0

    Combinatorial game library in Lean 4

  19. dwrensha/compfilesuses2507836

    Catalog Of Math Problems Formalized In Lean

  20. Timeroot/computableRealuses003ff45

    computable implementation of real numbers in Lean4