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.

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.

「The Lean Language Reference」の日本語訳（作業中）

Repositório destinado às práticas de Lean4 da Monitoria de FMCn.

The math library of Lean 4

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

The matrix cookbook, proved in the Lean theorem prover

A Foreign Function Interface (FFI) to cvc5 solver in Lean.

This project is about formally verifying Seymour's decomposition theorem for regular matroids.

Formalisation of the Cambridge Part II and Part III courses Graph Theory, Combinatorics, Extremal and Probabilistic Combinatorics in Lean

Catalog Of Math Problems Formalized In Lean

A minimal development of SSA theory

Lean4 Logic Formalization