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.

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

Scientific computing in Lean 4

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

Formalising Mathematics; a course for undergraduate mathematicians. Ran between January and March 2024.

Combinatorial game library in Lean 4

Formalization of "Analysis I" by Terence Tao

Sqlite3 bindings for lean4

Formalisation of toric varieties in Lean 4

A verifier for automated and interactive proofs about transition systems. This repository is a public mirror with stable development snapshots. Submit issues and PRs here.

Algebra library for Lean 4

Formalizing Value Distribution Theory

Code for the course "Proofs and Programs", January 2025, IISc

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

A minimal development of SSA theory

The math library of Lean 4

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

Central limit theorem in Lean

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

blueprint for prime number theorem and more

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

Repository for formalization of the Polynomial Freiman Ruzsa conjecture (and related results)

Raylib bindings for Lean4

The Lean reference manual