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 math library of Lean 4

A minimal development of SSA theory

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

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

Leaff is a diff tool for Lean environments

プログラミング言語であるとともに定理証明支援系でもある Lean 言語と、その主要なライブラリの使い方を豊富なコード例とともに解説した資料です。

Armv8 Native Code Symbolic Simulator in Lean

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