BibtexQuery
A simple command-line bibtex query utility written in Lean 4
1-20 of 50 packages depending on dupuisf/BibtexQuery
Sort by
Package Name
Verified-zkEVM/Arklibuses
v4.19.0-rc1Formally Verified Arguments of Knowledge in LeanJobPetrovcic/ArtinWedderburnuses
982700bA formalized proof of Artin-Wedderburn theorem in Lean4Bergschaf/banach_tarskiuses
bd8747dRikHeurter/BscThesisFormalisationuses
v4.19.0-rc1morganfshirley/CommCompuses
0a294feFormalization of communication complexity in Leanleanprover-community/ConNFuses
v4.19.0-rc1A formal consistency proof of Quine's set theory New FoundationsShreyas4991/DGAlgorithmsuses
c07de33Distributed Graph Algorithms in Leanleanprover/doc-gen4uses
v4.27.0-rc1Document Generator for Lean 4teorth/equational_theoriesuses
v4.19.0-rc1A project to map out the relations between different equational theories of Magmas.vikraman/event-structuresuses
v4.27.0-rc1Formalisation of some facts about event structures and reversibilitykkytola/ExtremeValueProjectuses
1b05159A project to formalize Fisher-Tippett-Gnedenko theorem (default project of course MS-EV0029)ivankobe/FactorizationSystemsuses
982700bleanprover-community/flt-regularuses
v4.27.0-rc1Fermat's Last Theorem for regular primesmo271/FormalBookuses
1b05159Formalizing "Proofs from THE BOOK"FormalizedFormalLogic/Foundationuses
29a4b34Formalization of Mathematical LogicWuProver/groebneruses
1b05159Formalization of Gröbner basis theory in Lean4 (WIP)mariovagomarzal/HigherCategoryTheoryuses
1b05159A formal verification project based on the work by Enric Cosme Llópez on "Higher-order categories".mkaratarakis/HopfieldNetuses
v4.27.0-rc1acmepjz/Iwasawalibuses
3ab4379Formalization of Iwasawa Theory in LꓱꓯN (tentative)riccardobrasca/Kaplansky4uses
9f78601Proof of Kaplanski criterion for being a UFD in Lean4