The math library of Lean 4

Transfinite nimber calculator in C++

A project to digitalise results from physics into Lean.

Package registry for Lean/Lake.

Lean formalization of the Kolmogorov extension theorem

Finds, Filters, and translates Chinese AI progress news

Truly independent web browser

Combinatorial game library in Lean 4

raw maxwell models and maxwell fan website

Try a tactic at each step in a Lean proof.

computable implementation of real numbers in Lean4

guess it. by name. good luck

A blueprint for a formalization of infinity-cosmos theory in Lean.

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

The Lean reference manual

A crate for mucking around with piles of bytes

The "batteries included" extended library for the Lean programming language and theorem prover

Mathlib search tool

Disproof of the Aharoni–Korman conjecture

A translation framework for eliminating definitional equalities in Lean

A formalization of PCF theory in lean

Ongoing Lean formalisation of the proof of Fermat's Last Theorem

Climb into Cantor’s Attic, where you will find infinities large and small. We aim to provide a comprehensive resource of information about all notions of mathematical infinity.

Natural Number Game

Official Flash Flash Revolution game engine.