doc-gen4
Document Generator for Lean 4
of 39 packages depending on leanprover/doc-gen4
1-20Sort by
Package Name
FR-vdash-bot/algorithmuses
v4.13.0-rc1
Verified efficient algorithms in Lean4.FormalizedFormalLogic/arithmetizationuses
b941c42
Formalization of Arithmetization of Mathematics/Metamathematicsfpvandoorn/bonnAnalysisuses
194403b
repository for the collaborative formalization seminar in Analysis in Bonnfpvandoorn/carlesonuses
v4.12.0
A formalized proof of Carleson's theorem in LeanYaelDillies/ChandraFurstLiptonuses
1b0072f
Formalisation in the Lean theorem prover of the relation between corner-free sets and communication complexityRemyDegenne/cltuses
1b0072f
Central limit theorem in Leanmorganfshirley/CommCompuses
1b0072f
Formalization of communication complexity in Leanleanprover-community/ConNFuses
v4.12.0
A formal consistency proof of Quine's set theory New Foundationsoptsuite/convexuses
d1be57c
teorth/equational_theoriesuses
v4.13.0-rc1
A project to map out the relations between different equational theories of Magmas.teorth/expdbuses
v4.13.0-rc1
Exponent pair databaseImperialCollegeLondon/FLTuses
v4.13.0-rc1
Ongoing Lean formalisation of the proof of Fermat's Last Theoremleanprover-community/flt-regularuses
1b0072f
Fermat's Last Theorem for regular primesmo271/FormalBookuses
1b0072f
Formalizing "Proofs from THE BOOK"HEPLean/hep_leanuses
v4.12.0
A project to digitalise results from high energy physics into Lean.mortarsanjaya/IMOSLLean4uses
1b0072f
Formalization of IMO shortlist problems in Lean 4FormalizedFormalLogic/Incompletenessuses
b941c42
Formalize Incompleness Theorem Related Resultsemilyriehl/InfinityCosmosuses
v4.13.0-rc1
A blueprint for a formalization of infinity-cosmos theory in Lean.SchrodingerZhu/lean-gccjituses
649e779
libgccjit bindings for Lean4YaelDillies/LeanAPAPuses
v4.13.0-rc1
Formalisation of the Kelley-Meka bound on Roth numbers