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

A "code intepreter" for Lean

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

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

Raylib bindings for Lean4

Low level utils (single precision float, byte spans, unboxed vector, finalization callbacks, fixnums, deque, slotmap etc; implemented via ffi)

Exponent pair database

A minimal development of SSA theory

Tools based on AI for helping with Lean 4

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

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

Catalog Of Math Problems Formalized In Lean