The math library of Lean 4

LLMs as Copilots for Theorem Proving in Lean

Lean theorem proving interface which feels like pen-and-paper proofs.

Scientific computing in Lean 4

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

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

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

White-box automation for Lean 4

Tutorial on neural theorem proving

Lean 4 port of the Verified Quantum Computing. Developed as a personal learning project to deepen understanding of quantum computing concepts and formal verification.

Bindings and specification for BLAS

Special Numbers (Chapter 6 from Knuth's Concrete Mathematics)

A Lean 4 formalization of partial combinatory algebras.

Lean coding problem solving challenge website with proof verification

Lean formalisation of the classification of the groups of order `p * q` where `p` and `q` are prime numbers.

「The Lean Language Reference」の日本語訳（作業中）

The math library of Lean 4

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

A (WIP) equality saturation tactic for Lean based on egg.

Advent of Code

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

Mathlib search tool

A project to digitalise results from high energy physics into Lean.

Try a tactic at each step in a Lean proof.

Document Generator for Lean 4