## BibtexQuery

A simple command-line bibtex query utility written in Lean 4

**1-20**of

**29**packages depending on

**dupuisf/BibtexQuery**

Sort by

Package Name

### FR-vdash-bot/algorithmuses

`85e1e71`

Verified efficient algorithms in Lean4.### fpvandoorn/carlesonuses

`85e1e71`

A formalized proof of Carleson's theorem in Lean### YaelDillies/ChandraFurstLiptonuses

`0a294fe`

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

`0a294fe`

Central limit theorem in Lean### morganfshirley/CommCompuses

`0a294fe`

Formalization of communication complexity in Lean### leanprover-community/ConNFuses

`85e1e71`

A formal consistency proof of Quine's set theory New Foundations### leanprover/doc-gen4uses

`bdc2fc3`

Document Generator for Lean 4### teorth/equational_theoriesuses

`85e1e71`

A project to map out the relations between different equational theories of Magmas.### teorth/expdbuses

`bdc2fc3`

Exponent pair database### ImperialCollegeLondon/FLTuses

`bdc2fc3`

Ongoing Lean formalisation of the proof of Fermat's Last Theorem### leanprover-community/flt-regularuses

`85e1e71`

Fermat's Last Theorem for regular primes### mo271/FormalBookuses

`85e1e71`

Formalizing "Proofs from THE BOOK"### HEPLean/hep_leanuses

`85e1e71`

A project to digitalise results from high energy physics into Lean.### mortarsanjaya/IMOSLLean4uses

`0a294fe`

Formalization of IMO shortlist problems in Lean 4### emilyriehl/InfinityCosmosuses

`bdc2fc3`

A blueprint for a formalization of infinity-cosmos theory in Lean.### YaelDillies/LeanAPAPuses

`bdc2fc3`

Formalisation of the Kelley-Meka bound on Roth numbers### YaelDillies/LeanCamCombiuses

`bdc2fc3`

Formalisation of the Cambridge Part II and Part III courses Graph Theory, Combinatorics, Extremal and Probabilistic Combinatorics in Lean### JamesGallicchio/leancollsuses

`c138ab5`

WIP collections library for Lean 4### fpvandoorn/LeanCourseuses

`85e1e71`

Bonn Lean course for winter 24/25### leanprover/lnsymuses

`85e1e71`

Armv8 Native Code Symbolic Simulator in Lean