checkdecls
Tiny Lean library to check existence of declarations
of 43 packages depending on PatrickMassot/checkdecls
1-20Sort by
Package Name
b-mehta/ABCExceptionsuses
lean4.18.0
Exceptions to the ABC conjecture in LeanVerified-zkEVM/Arklibuses
lean4.18.0
Formally Verified Arguments of Knowledge in LeanJobPetrovcic/ArtinWedderburnuses
11fa569
A formalized proof of Artin-Wedderburn theorem in Lean4fpvandoorn/bonnAnalysisuses
21a36f3
repository for the collaborative formalization seminar in Analysis in BonnRemyDegenne/BrownianMotionuses
lean4.18.0
Construction of a Brownian Motion in LeanRikHeurter/BscThesisFormalisationuses
lean4.18.0
fpvandoorn/carlesonuses
lean4.18.0
A formalized proof of Carleson's theorem in LeanYaelDillies/ChandraFurstLiptonuses
lean4.18.0
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
lean4.18.0
A project to map out the relations between different equational theories of Magmas.teorth/expdbuses
lean4.18.0
Exponent pair databasekkytola/ExtremeValueProjectuses
lean4.18.0
A project to formalize Fisher-Tippett-Gnedenko theorem (default project of course MS-EV0029)ivankobe/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
lean4.18.0
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.