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.

A minimal development of SSA theory

Formalization of the existence of sphere eversions

Tableaux for Propositional Dynamic Logic in Lean 4 (WORK IN PROGRESS)

The math library of Lean 4

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

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

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

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

Executable formal model of the EVM and Yul in Lean 4.