## UnicodeBasic

Basic Unicode support for Lean 4

**1-20**of

**44**packages depending on

**fgdorais/UnicodeBasic**

Sort by

Package Name

### FR-vdash-bot/algorithmuses

`v1.0.2`

Verified efficient algorithms in Lean4.### dupuisf/BibtexQueryuses

`7afce91`

A simple command-line bibtex query utility written in Lean 4### fpvandoorn/bonnAnalysisuses

`c74a052`

repository for the collaborative formalization seminar in Analysis in Bonn### fpvandoorn/carlesonuses

`v1.0.2`

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

`7afce91`

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

`7afce91`

Central limit theorem in Lean### morganfshirley/CommCompuses

`7afce91`

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

`v1.0.2`

A formal consistency proof of Quine's set theory New Foundations### optsuite/convexuses

`c74a052`

### leanprover/doc-gen4uses

`107e98b`

Document Generator for Lean 4### teorth/equational_theoriesuses

`v1.0.2`

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

`107e98b`

Exponent pair database### ImperialCollegeLondon/FLTuses

`107e98b`

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

`v1.0.2`

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

`v1.0.2`

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

`v1.0.2`

A project to digitalise results from high energy physics into Lean.### JamesGallicchio/Httpuses

`8603bb1`

Basic HTTP definitions and parsing for Lean### mortarsanjaya/IMOSLLean4uses

`7afce91`

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

`107e98b`

A blueprint for a formalization of infinity-cosmos theory in Lean.### SchrodingerZhu/lean-gccjituses

`f092502`

libgccjit bindings for Lean4