Lean 3's obsolete mathematical components library: please use mathlib4

A collection of formalized statements of conjectures in Lean.

LLMs as Copilots for Theorem Proving in Lean

The matrix cookbook, proved in the Lean theorem prover

A template for blueprint-driven formalization projects in Lean.

Solutions to Imperial College London's Natural Number Game, a gamified formal mathematics course on the Peano axioms using an interactive + automated theorem prover developed by Microsoft Research called Lean.

The first comprehensive Lean 4 formalization of statistical learning theory, featuring Gaussian Lipschitz concentration and Dudley's entropy integral-establishes a reusable foundation for formalizing ML theory.

The Principia Rewrite

Repository hosting the resources for the conference "ItaLean 2025", held in Bologna, Italy, December 9–12, 2025.

Repository hosting resources for the "Lean Tutorial in Vienna" at TU Wien from September 18 to 20, 2024.

Formalising the paper "Sums of Three Squares" by N. C. Ankeny in Lean with Aristotle.

The Slate Interactive Theorem Prover

A formalised proof of Fermat's Last Theorem for exponent 3 in the Lean proof assistant.

Lean formalizations of IMO problem statements

rubikcubegroup魔方定理证明+视频分享。discuss here: https://lean4daydayup.zulipchat.com/join/45reytdk5yv7t7sheywhulw3/

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

matroids in lean

HLM mathematical library for the Slate interactive theorem prover

mai: MAth Interpreter with Standard Foundations

Formalising the Ring of Integers in Quadratic Fields in the Lean proof assistant.