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.

A minimal development of SSA theory

A formalized proof of Carleson's theorem in Lean

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

The math library of Lean 4

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

Natural language tactics to teach mathematics using Lean 4

A project to digitalise results from high energy physics into Lean.

Formalisms Every Computer Scientist Should Know (course at ISTA)

Advent of Code

Experiments in automation for Lean