checkdecls
Tiny Lean library to check existence of declarations
of 31 packages depending on PatrickMassot/checkdecls
1-20Sort by
Package Name
Verified-zkEVM/Arklibuses
lean4.18.0
Formally Verified Arguments of Knowledge in Leanfpvandoorn/bonnAnalysisuses
21a36f3
repository for the collaborative formalization seminar in Analysis in Bonnfpvandoorn/carlesonuses
lean4.18.0
A formalized proof of Carleson's theorem in LeanYaelDillies/ChandraFurstLiptonuses
11fa569
Formalisation in the Lean theorem prover of the relation between corner-free sets and communication complexityRemyDegenne/cltuses
lean4.18.0
Central limit theorem in LeanShreyas4991/DGAlgorithmsuses
lean4.18.0
Distributed Graph Algorithms in Leanteorth/equational_theoriesuses
8e459c6
A project to map out the relations between different equational theories of Magmas.teorth/expdbuses
lean4.18.0
Exponent pair databaseivankobe/FactorizationSystemsuses
11fa569
ImperialCollegeLondon/FLTuses
lean4.18.0
Ongoing Lean formalisation of the proof of Fermat's Last Theoremleanprover-community/flt-regularuses
lean4.18.0
Fermat's Last Theorem for regular primesriccardobrasca/flt-regularuses
75d7aea
Proof of Kaplanski criterion for being a UFD in Lean4mo271/FormalBookuses
11fa569
Formalizing "Proofs from THE BOOK"WuProver/groebneruses
lean4.18.0
Formalization of Gröbner basis theory in Lean4 (WIP)emilyriehl/InfinityCosmosuses
lean4.18.0
A blueprint for a formalization of infinity-cosmos theory in Lean.acmepjz/Iwasawalibuses
lean4.18.0
Formalization of Iwasawa Theory in LꓱꓯN (tentative)Bergschaf/LeanBanachTarskiuses
75d7aea
Bergschaf/leroyuses
75d7aea
loganrjmurphy/libuses
lean4.18.0
LeanEuclid is a benchmark for autoformalization in the domain of Euclidean geometry, targeting the proof assistant Lean.pitmonticone/NewProjectuses
11fa569