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

LLMs as Copilots for Theorem Proving in Lean

A collection of formalized statements of conjectures in Lean.

The Principia Rewrite

The matrix cookbook, proved in the Lean theorem prover

A template for blueprint-driven formalization projects in Lean.

[ICML2026] The first, fully verified, sorry-free, large-scale Lean 4 library for statistical learning theory, covering infrastructures for mordern statistics and learning theory.

Lean formalizations of IMO problem statements

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

The Slate Interactive Theorem Prover

A curated list of awesome interactive theorem prover frameworks

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.

A style guide for Coq

AI-powered IDE for Lean 4 theorem proving. Integrates Claude as a proof assistant with full tool use, live tactic state, inline diagnostics, Unicode input, and Lake build support. Built with Flutter.

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

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

A fork of openai/miniF2F adapted to Lean 4, with corrections to formalizations and informal descriptions. for human readers.

A kernel-minimal LCF-style HOL theorem prover in the Wolfram Language

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

Number representation when the base is a free parameter — a machine-checked corpus on function-defined radix systems, from positional notation as algebra to the geometry and conservation laws of coupled radix networks.