Lean 4 programming language and theorem prover

The math library of Lean 4

A Lean companion to Analysis I

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

A project to digitalise results from physics into Lean.

Metamath Zero specification language

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

Catalog Of Math Problems Formalized In Lean

LLMs + Lean, on your laptop or in the cloud

A simple raytracer written in Lean 4

A zero-knowledge Lean4 compiler and kernel

Lean circuit DSL

Natural language tactics to teach mathematics using Lean 4

SampCert : Verified Differential Privacy

tool for turning Lean proofs into Blender animations

Beginner's guide to Tactic Programming in Lean

Experiments with SAT solvers with proofs in Lean 4

Fermat's Last Theorem for regular primes

A library of results from Social Choice Theory, formalized in the Lean Theorem Prover.

Chess in Lean 4

Formalization of the Rupert Problem for convex polyhedra.

Automata theory in Lean

Formalization of Statement of Local Langlands Correspondence for Tori

Advent of Code