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 Verification (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.