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.

The Slate Interactive Theorem Prover

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

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

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

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

A formalization of graded rings in Lean, corresponding to a CICM 2022 submission

Library for formalizing cryptography proofs in Lean 3 (Deprecated)

matroids in lean

mai: MAth Interpreter with Standard Foundations

HLM mathematical library for the Slate interactive theorem prover

Repository hosting the resources for the Lean demo session of my talk presented at the weekly research seminar on CHallenges in ANalysis and GEometry (CHANGE) at the University of Trento on February 11, 2025.

LLMs + Lean, on your laptop or in the cloud

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