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.

A formalized proof of Carleson's theorem in Lean

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.

Morse Code training application for Android

An interface between Lean4 and Oscar.

A complete implementation of 10918-1 (JPEG) coming from jpeg.org (the ISO group) with extensions for HDR, lossless and alpha channel coding standardized as ISO/IEC 18477 (JPEG XT).

Try a tactic at each step in a Lean proof.

Repo for the first BerLean workshop.

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

`xrandr` for Gnome/wayland, on distros that don't support `wlr-randr`

lightweight, standalone C++ inference engine for Google's Gemma models.

An attempt at formalizing facts on Euler products in Lean

blueprint for prime number theorem and more

The Lean version manager