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

Algebra library for Lean 4

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

The math library of Lean 4

A minimal development of SSA theory

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

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

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

Experiments in automation for Lean

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

A blueprint for a formalization of infinity-cosmos theory in Lean.

LLMs as Copilots for Theorem Proving in Lean

A formalization of the NKI ISA