# Lean

Open source theorem prover and programming language being developed at Microsoft Research.

Natural number game, Mathematics in Lean tutorial, Functional Programming in Lean & Theorem Proving in Lean 4 are great.

## Links

- Theorem Proving in Lean 4
- Theorem Proving in Lean (Solutions) (PDF)
- Xena - Lean Library currently studying for a degree at Imperial College.
- Xena Project - Building a library of undergraduate level pure maths.
- Lean mathlib - Lean mathematical components library.
- The Lean mathematical library paper
- lean-perfectoid-spaces - Perfectoid spaces in the Lean formal theorem prover.
- Using Lean with undergraduate mathematicians (2019)
- What does Lean already know?
- lean-category-theory - Experimental category theory library for Lean.
- Lean explained by nLab
- Maths in Lean : category theory
- TypeTheory - Mathematical study of type theories, in univalent foundations.
- M4P33 - Algebraic geometry course in Lean.
- Lean 4 code (HN)
- Lean 3 code
- Doing a math assignment with the Lean theorem prover (2020)
- Hitchhiker’s Guide to Logical Veriﬁcation (HN)
- Natural Number Game (HN) (Code)
- Certigrad - Bug-free machine learning on stochastic computation graphs.
- Ellen's dots and boxes project - Contains all the code written for my final year research project in Mathematics, "Optimal gameplay in Dots and Boxes in Lean".
- Building the Mathematical Library of the Future (2020)
- A Review of the Lean Theorem Prover (2018) (HN)
- Lean Together 2021 - Meeting for Lean users and other formalizers. (Code)
- Advent of Code 2020 puzzles in Lean 4
- Schemes in Lean (2021)
- Quantum Computing in Lean - Formalized quantum computing in Lean theorem prover.
- lean-gptf - Interactive neural theorem proving in Lean.
- Flypitch - Formal proof of the independence of the continuum hypothesis. (Web)
- Monadic parser combinators, in Lean
- elan - Lean version manager.
- Lean Community (Code)
- Simple ray tracer in Lean 4 (HN)
- Ground Zero - Provides computable HITs, variation of Cubical Type Theory using them, and some other math.
- Lean HOL - Tiny implementation of higher-order logic proof assistant in lean.
- Formal [Lean] Proof of the Independence of the Continuum Hypothesis (2021)
- Formalising Mathematics: An Introduction (2021) (HN)
- lean4-cli - A Lean 4 library for configuring Command Line Interfaces and parsing command line arguments. (Fork)
- Lean reference type-checker
- Formal ML - LEAN library for proving foundational results in measure theory, probability, statistics, and machine learning, based upon mathlib.
- Lean 4 course Theorem prover lab: applications in programming languages
- “Lean” Computer Program Confirms Peter Scholze Proof (2021)
- lean.nvim - Neovim support for the Lean theorem prover.
- Elements of Differential Geometry in Lean: A Report for Mathematicians (2021)
- quote4 - Intuitive, type-safe expression quotations for Lean 4.
- leanprover-contrib - Basic checkin/CI for Lean projects that are not part of mathlib.
- mathlib4 - Mathlib port for Lean 4.
- Brown CS 1951x: Formal Proof and Verification, 2021 (Code)
- Introduction to University Mathematics Course: using Lean (2021)
- Mathport - Tool for porting Lean3 projects to Lean4.
- Lean Tutorials
- lean-gym - Interact with Lean through a REPL.
- How Lean compares to Coq/Isabelle/HOL
- SATurn - SAT solver-prover in lean 4 based on the DPLL algorithm.
- Aesop - White-box automation for Lean 4.
- doc-gen4 - Document Generator for Lean 4.
- Lean formal proof of the Combinatorial Nullstellensatz
- Alloy - Lean 4 library that allows one to embedded external FFI code (currently just C) within Lean definitions.
- Lean SAT Proof Checker
- NumLean - Lean 4 package for heavy numerical computations.
- tree-sitter-lean - Experimental tree-sitter parser for Lean.
- Inductive-Inductive Types for Lean 4
- SciLean - Framework for scientific computing written in Lean.
- Lean4 Postgresql Frontend-Backend-protocol
- Data Types as Quotients of Polynomial Functors
- Unit fractions
- Topos theory for Lean
- Lean for the Curious Mathematician 2020 (Web)
- Ground Zero - Library provides computable HITs, variation of Cubical Type Theory using them, and some other math.
- Lean 4 Metaprogramming Book
- Lean verbose - Controlled natural language tactics for Lean.
- BUM - Lean 4 Package Manager.
- Simple bidirectional type-checker in Lean 4
- Maze game encoded in Lean 4 syntax
- Model and framework to prove formal semantics of MLIR programs in Lean4
- Protocol buffers in Lean 4
- GAP-LEAN - GAP parser, pretty printer, interpreter, and formal semantics.
- Cryptography in Lean 4
- OpenGL Lean bindings
- Fermat's Last Theorem for regular primes
- Lean-to - Jupyter shelter for your Lean4 code.
- Lean 4 as a scripting language in Houdini
- HTTP.lean - Uses Socket.lean to create basic HTTP functionality.
- Lean 4 Socket - Implementation of socket programming for Lean 4.
- Unicode.lean - Unicode related operations for Lean 4.
- Parsec.lean - Parser combinators for Lean.
- Nix expressions and derivations in lean
- doc-gen4 - Document Generator for Lean 4.
- lean4-karray - Package that allows automatic C code generation for functions defined in Lean.
- Lean material for Kevin Buzzard's Jan-Mar 2022 course on formalizing mathematics
- Formalization of Gardam's disproof of the unit conjecture in Lean
- Lean Ipld - Lean4 implementation of the IPLD format.
- Functional Programming in Lean (HN)
- Lake - Lean 4 build system and package manager with configuration files written in Lean.
- Lean-Chat - OpenAI Codex-powered chat interface for translating natural language theorem statements into Lean mathlib.
- Lean Game Maker - Library renders structured Lean files into an interactive game with a JS Lean server running on the browser.
- Lean formalization of parts of Martin Liebeck's "A concise introduction to pure mathematics"
- Experimenting with Lean 4
- Proof artifact co-training on Lean mathlib
- Lean chat - Chat with OpenAI Codex to generate formal theorem statements in Lean for you.
- Lean 4 interface to Eigen
- std4 - Standard Library for Lean 4.
- Beyond the Liquid Tensor Experiment (2022)
- LeanAide - Tools based on AI for helping with Lean 4.
- Formal BOOK - Collaborative, work-in-progress attempt to formalize Proofs from THE BOOK using Lean.
- Collections for Lean 4
- Proofs written in Lean4 for the core katydid validation algorithm
- Theorem Proving in Lean 4
- Tests around generalized rewriting in Lean 4
- WASM Lean - WebAssembly tools for Lean.
- Lean 4 Poseidon implementation
- Zulip Chat Archive
- FFI.lean - Template for calling Rust functions in Lean using C/C++ FFI and the CXX crate.
- LSpec - Testing framework for Lean 4, inspired by Haskell's Hspec package.
- Advent of Code 2022 in Lean
- Infinitude of primes --- a Lean theorem prover demo (2020)
- mlir-lean - Embedded MLIR in LEAN.
- Parser for ANSI C, in Lean 4
- Formalization of DBSP in Lean
- Mechanizing Modern Mathematics (2023)
- HN: Lean (2023)
- WidgetKit - Library of user interface components for Lean 4.
- LeanInk - Command line helper tool for Alectryon which aims to ease the integration of Lean 4.
- Mathematics in Lean (Code)
- Classical Mechanics Lean
- Code samples for Lean 4
- Megaparsec - Lean 4 port of Megaparsec.
- Lean course from Brown uni (2023)
- SSA in Lean - Theory of static single assignment development in Lean.
- Leonardo de Moura - The Lean proof assistant: introduction and challenges (2023)
- ExtParser - Extensible Grammar Parser.
- Lean 4 Game - Prototype for a Lean 4 game platform.
- Interfacing with Large Language Models (remote and local) from Lean
- Lean 4 port of Iris - Higher-order concurrent separation logic framework.
- Uniq - Static Uniqueness Analysis for the Lean 4 Theorem Prover.
- risc0-lean4 - Model of the RISC Zero zkVM and ecosystem in the Lean 4 Theorem Prover.
- Lecture notes for a course on writing proofs, on paper and in the Lean proof assistant
- LeanDojo - Tool for data extraction and interacting with Lean programmatically.
- ReProver - Retrieval-Augmented Theorem Provers for Lean.
- Functional Programming in Lean
- Leetcode exercises in Lean4
- Playing sudoku in the Lean theorem prover
- LeanInfer - Neural Network Inference in Lean 4.