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.

A verifier for automated and interactive proofs about transition systems. This repository is a public mirror with stable development snapshots. Submit your 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.

Formally Verified SNARKs in Lean

Bindings and specification for BLAS

Juvix Lean library for compiler run verification

The math library of Lean 4

Lean documentation authoring tool

A project to digitalise results from physics into Lean. (formally called HepLean)

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

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

Utilities for formalizing programming languages in Lean 4, along with other tidbits

LLMs as Copilots for Theorem Proving in Lean

Scientific computing in Lean 4

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