full feature async redis client for lean 4

Stub: planned Lean 4 FFI bindings for SoPlex (iterative-refinement exact LP). PLAN.md only.

Lean Bzip2 compression library using Burrows Wheeler Transformation.

Lean for Huffmann Coding Algorithms, as a course Project for Proof and Programs 25.

The sublibrary of Mathlib dedicated to additive combinatorics

Automatically proving computability for Lean functions

SQLite bindings for Lean

A YAML 1.2.2 parser in Lean 4 with the goal of **verified correctness**

Lean 4 Markdown rendering library — types, rendering functions, and Represent typeclass

A working definition of a peer-reviewed formalization

Co-inductive datatypes for Lean

Github repository for the 2025 Clay Summer School on Formalizing Class Field Theory

Formalization of Gröbner basis theory in Lean4 (WIP)

A formalization project of set theory and elementary embeddings in Lean 4. Includes a proof of Kunen's inconsistency theorem.

Scripts and utilities to support the mathlib repository's CI/CD operations

Hosts the website for mathlib and other Lean community infrastructure.

Plain-text declaration export for Lean 4

a Lean wrapper for the MD4C Markdown parser

Formalizing results about the Mandelbrot set in Lean

Server to host Lean games

Formal proof of the Four Color Theorem [maintainer=@ybertot]

This repository preserves the `cc` tactic that was once in Mathlib

Agda is a dependently typed programming language / interactive theorem prover.

Floating Point Semantics Mechanization for Lean