Some Lean proofs

AlphaZero implemented for Hex

A collection of formalized statements of conjectures in Lean.

Content of Online Encyclopedia of Integer Sequences (OEIS)

Lean formalizations of Putnam-like problems

SorryDB indexes sorries in public lean repositories

Leaff is a diff tool for Lean environments

A community database for the problems on the erdosproblems.com site

A formalized proof of Carleson's theorem in Lean

ICC color profiles in Rust

Code to automatically prove or verify estimates in analysis

A programming font focused on source code legibility

Formalisation of the Kelley-Meka bound on Roth numbers

A Lean proof that there exist Principal Ideal Domains which do not have a Euclidean function

Lean documentation authoring tool

ASCII/Unicode plotting library for Lean 4 with legends and braille rendering

Problems and Results of IWLS 2022 Programming Contest

A minimalist property-based testing library

Pure Rust implementation of JPEG XL decoder

Formalizing "Proofs from THE BOOK"

Proofs from THE BOOK written up in lean

A project to map out the relations between different equational theories of Magmas.

Pillow plugin for JPEG-XL, using Rust for bindings.

Chess in Lean 4

A Lean 4 representation of the Rubik's Cube, some proofs about the representation, and a simple solution algorithm.

tool for turning Lean proofs into Blender animations

The OpenEXR project provides the specification and reference implementation of the EXR file format, the professional-grade image storage format of the motion picture industry.

Tool to analyse the import structure of lean projects.