GitHub topics: lean4
Julian/lean.nvim
Neovim support for the Lean theorem prover
Language: Lua - Size: 2.01 MB - Last synced at: about 3 hours ago - Pushed at: about 4 hours ago - Stars: 350 - Forks: 31
ufmg-smite/lean-smt
Tactics for discharging Lean goals into SMT solvers.
Language: Lean - Size: 788 KB - Last synced at: about 6 hours ago - Pushed at: about 7 hours ago - Stars: 176 - Forks: 22
oOo0oOo/leanclient
Python client to interact with the lean4 language server.
Language: Python - Size: 3.7 MB - Last synced at: about 11 hours ago - Pushed at: about 11 hours ago - Stars: 12 - Forks: 0
fgdorais/extra4
Supplements to the Lean 4 Standard Library
Language: Lean - Size: 173 KB - Last synced at: about 19 hours ago - Pushed at: about 20 hours ago - Stars: 3 - Forks: 0
fgdorais/lean4-parser
Parser Combinator Library for Lean 4
Language: Lean - Size: 9.66 MB - Last synced at: about 19 hours ago - Pushed at: about 20 hours ago - Stars: 49 - Forks: 6
JadAbouHawili/KnightsAndKnaves-Lean4Game
Knights and Knaves Educational Game in Lean 4
Language: Lean - Size: 1.02 MB - Last synced at: 1 day ago - Pushed at: 1 day ago - Stars: 3 - Forks: 2
oOo0oOo/lean-lsp-mcp
Lean Theorem Prover MCP
Language: Python - Size: 204 KB - Last synced at: 1 day ago - Pushed at: 1 day ago - Stars: 22 - Forks: 1
dwrensha/compfiles
Catalog Of Math Problems Formalized In Lean
Language: Lean - Size: 2.21 MB - Last synced at: 1 day ago - Pushed at: 1 day ago - Stars: 152 - Forks: 28
FormalizedFormalLogic/Foundation
Formalization of Mathematical Logic
Language: Lean - Size: 5.65 MB - Last synced at: about 20 hours ago - Pushed at: about 21 hours ago - Stars: 116 - Forks: 6
shnarazk/learn
Self learning by doing
Language: Lean - Size: 14.1 MB - Last synced at: 1 day ago - Pushed at: 1 day ago - Stars: 0 - Forks: 0
leanprover-community/con-nf
A formal consistency proof of Quine's set theory New Foundations
Language: Lean - Size: 18.2 MB - Last synced at: 1 day ago - Pushed at: 2 days ago - Stars: 70 - Forks: 7
Ivan-Sergeyev/seymour
This project is about formally verifying Seymour's decomposition theorem for regular matroids.
Language: Lean - Size: 9.22 MB - Last synced at: 2 days ago - Pushed at: 2 days ago - Stars: 23 - Forks: 7
leanprover/lean-action
GitHub action for standard CI in Lean projects
Language: Shell - Size: 204 KB - Last synced at: 1 day ago - Pushed at: 17 days ago - Stars: 19 - Forks: 6
nomeata/loogle
Mathlib search tool
Language: Lean - Size: 301 KB - Last synced at: 2 days ago - Pushed at: 2 days ago - Stars: 86 - Forks: 18
dwrensha/Rupert.lean
Formalization of the Rupert Problem for convex polyhedra.
Language: Lean - Size: 136 KB - Last synced at: 2 days ago - Pushed at: 2 days ago - Stars: 3 - Forks: 1
shnarazk/DDiL
BDD and ZDD in Lean4
Language: Lean - Size: 264 KB - Last synced at: 2 days ago - Pushed at: 3 days ago - Stars: 0 - Forks: 0
shnarazk/advent-of-code
🎄The annual event for computer science enthusiasts!
Language: Rust - Size: 5.06 MB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 5 - Forks: 2
mtoohey31/lott
An ott-like DSL embedded in Lean.
Language: Lean - Size: 210 KB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 1 - Forks: 1
leanprover-community/aesop
White-box automation for Lean 4
Language: Lean - Size: 4 MB - Last synced at: 1 day ago - Pushed at: 9 days ago - Stars: 266 - Forks: 32
Anderssorby/SDL.lean
SDL2 bindings for lean
Language: Lean - Size: 134 KB - Last synced at: 1 day ago - Pushed at: about 1 year ago - Stars: 22 - Forks: 4
project-numina/kimina-lean-server
Kimina Lean server
Language: Python - Size: 1.05 MB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 53 - Forks: 3
dmavani25/chip-firing-with-lean
A formalization of chip-firing games and the Riemann-Roch theorem for graphs using the Lean 4 theorem prover.
Language: Lean - Size: 340 KB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 1 - Forks: 0
fgdorais/lean4-unicode-basic
Basic Unicode support for Lean 4
Language: Lean - Size: 10.9 MB - Last synced at: 1 day ago - Pushed at: 1 day ago - Stars: 9 - Forks: 5
leanprover-community/mathlib4
The math library of Lean 4
Language: Lean - Size: 366 MB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 1,923 - Forks: 411
objectionary/proof
Proof of 𝜑-calculus confluence
Language: Lean - Size: 4.48 MB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 7 - Forks: 1
jessealama/lean-decimals
Implementation & verification of exact decimal arithmetic in Lean 4
Language: Lean - Size: 62.5 KB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 0 - Forks: 0
augustepoiroux/LeanInteract
LeanInteract: A Python Interface for Lean 4
Language: Python - Size: 129 KB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 24 - Forks: 5
PatrickMassot/verbose-lean4
Natural language tactics to teach mathematics using Lean 4
Language: Lean - Size: 1.99 MB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 74 - Forks: 15
34j/best-of-lean4
A list of awesome lean4 projects. Feel free to add your project.
Size: 2.83 MB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 84 - Forks: 4
leanprover-community/ProofWidgets4
Helper toolkit for creating your own Lean 4 UserWidgets
Language: Lean - Size: 1.21 MB - Last synced at: 3 days ago - Pushed at: 9 days ago - Stars: 134 - Forks: 36
pitmonticone/LeanProject
Template for blueprint-driven formalization projects in Lean.
Language: Python - Size: 113 KB - Last synced at: 4 days ago - Pushed at: 13 days ago - Stars: 49 - Forks: 5
eric-wieser/lean-matrix-cookbook
The matrix cookbook, proved in the Lean theorem prover
Language: Lean - Size: 177 KB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 105 - Forks: 13
opencompl/fp.lean
Floating Point Semantics Mechanization for Lean
Language: Lean - Size: 3.11 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 0 - Forks: 0
madvorak/vcsp
General-Valued Constraint Satisfaction Problems
Language: Lean - Size: 1.21 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 9 - Forks: 1
stanford-centaur/PyPantograph
A Machine-to-Machine Interaction System for Lean 4.
Language: Python - Size: 46.8 MB - Last synced at: 5 days ago - Pushed at: 10 days ago - Stars: 80 - Forks: 18
fpvandoorn/carleson
A formalized proof of Carleson's theorem in Lean
Language: Lean - Size: 2.84 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 52 - Forks: 28
Seasawher/SelectionSort.lean
selection sort implemented and verified by lean
Language: Lean - Size: 101 KB - Last synced at: 6 days ago - Pushed at: 6 days ago - Stars: 0 - Forks: 0
vltanh/lean4-analysis-tao
Formalization of "Analysis I" by Terence Tao
Language: Lean - Size: 88.9 KB - Last synced at: 6 days ago - Pushed at: 6 days ago - Stars: 12 - Forks: 0
leanprover-community/batteries
The "batteries included" extended library for the Lean programming language and theorem prover
Language: Lean - Size: 17.5 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 299 - Forks: 118
leanprover-community/lean4game
Server to host lean games.
Language: TypeScript - Size: 32.9 MB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 256 - Forks: 44
leanprover/lean4
Lean 4 programming language and theorem prover
Language: Lean - Size: 2.03 GB - Last synced at: 6 days ago - Pushed at: 6 days ago - Stars: 5,441 - Forks: 570
siddhartha-gadgil/LeanAide
Tools based on AI for helping with Lean 4
Language: Jupyter Notebook - Size: 157 MB - Last synced at: 6 days ago - Pushed at: 7 days ago - Stars: 82 - Forks: 10
reilabs/lampe
Extracting the semantics of Noir to Lean for formal verification
Language: Lean - Size: 2.7 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 27 - Forks: 2
hrmacbeth/math2001
Lecture notes for a course on writing proofs, on paper and in the Lean proof assistant
Language: HTML - Size: 5.32 MB - Last synced at: 5 days ago - Pushed at: 5 months ago - Stars: 249 - Forks: 124
NaveenMaurya749/AutomataLean
This project aims to formalize some concepts of Automata Theory and Parsing into Lean4 Theorem Prover. This was a course project for the course 'Proofs and Programs' offered by Prof Siddhartha Gadgil at IISc, Spring 2025.
Language: Lean - Size: 18.6 KB - Last synced at: 7 days ago - Pushed at: 7 days ago - Stars: 0 - Forks: 0
pandaman64/lean-regex
Language: Lean - Size: 741 KB - Last synced at: 7 days ago - Pushed at: 7 days ago - Stars: 25 - Forks: 1
lftcm2023/lftcm2023
Language: Lean - Size: 217 KB - Last synced at: 2 days ago - Pushed at: over 1 year ago - Stars: 20 - Forks: 13
konnov/leanda
Distributed algorithms in Lean 4
Language: Lean - Size: 46.9 KB - Last synced at: 7 days ago - Pushed at: 7 days ago - Stars: 0 - Forks: 0
abdoo8080/lean-cvc5
A Foreign Function Interface (FFI) to cvc5 solver in Lean.
Language: Lean - Size: 276 KB - Last synced at: 7 days ago - Pushed at: 8 days ago - Stars: 14 - Forks: 4
loganrjmurphy/LeanEuclid
LeanEuclid is a benchmark for autoformalization in the domain of Euclidean geometry, targeting the proof assistant Lean.
Language: Lean - Size: 3.57 MB - Last synced at: 8 days ago - Pushed at: 8 days ago - Stars: 98 - Forks: 8
GasStationManager/SafeVerify
A Lean4 script for robustly verifying submitted proofs of theorems and implementations of functions
Language: Lean - Size: 45.9 KB - Last synced at: 6 days ago - Pushed at: 6 days ago - Stars: 3 - Forks: 0
Seasawher/mk-exercise
Simple and intuitive tool to manage exercises in textbooks written in Lean.
Language: Lean - Size: 94.7 KB - Last synced at: 8 days ago - Pushed at: 8 days ago - Stars: 7 - Forks: 0
Seasawher/mdgen
Tool to generate markdown files from lean files. This is heavily inspired by lean2md.
Language: Lean - Size: 149 KB - Last synced at: 8 days ago - Pushed at: 8 days ago - Stars: 17 - Forks: 2
Seasawher/lean-book
mdbook template for Lean project
Language: Lean - Size: 168 KB - Last synced at: 8 days ago - Pushed at: 8 days ago - Stars: 5 - Forks: 0
Seasawher/mathlib4-help
List of the output of #help command of mathlib4, including list of all tactics, commands...etc
Language: Python - Size: 5.41 MB - Last synced at: 8 days ago - Pushed at: 8 days ago - Stars: 17 - Forks: 1
chasenorman/CanonicalLean
A Lean tactic for Canonical, a search procedure for terms in dependent type theory.
Language: C - Size: 6.15 MB - Last synced at: 9 days ago - Pushed at: 9 days ago - Stars: 31 - Forks: 0
YaelDillies/add-combi
The (currently unofficial) sublibrary of Mathlib dedicated to additive combinatorics
Language: Shell - Size: 43 KB - Last synced at: 9 days ago - Pushed at: 9 days ago - Stars: 8 - Forks: 1
chasenorman/Canonical
Canonical is a performant sound and complete type inhabitation solver for dependent type theory.
Language: Lean - Size: 82 KB - Last synced at: 9 days ago - Pushed at: 9 days ago - Stars: 21 - Forks: 1
YaelDillies/LeanAPAP
Formalisation of the Kelley-Meka bound on Roth numbers
Language: Lean - Size: 1.41 MB - Last synced at: 9 days ago - Pushed at: 9 days ago - Stars: 17 - Forks: 7
girving/debate Fork of google-deepmind/debate
Formalizing stochastic doubly-efficient debate
Language: Lean - Size: 275 KB - Last synced at: 9 days ago - Pushed at: 9 days ago - Stars: 5 - Forks: 2
YaelDillies/LeanCamCombi
Formalisation of the Cambridge Part II and Part III courses Graph Theory, Combinatorics, Extremal and Probabilistic Combinatorics in Lean
Language: Lean - Size: 958 KB - Last synced at: 9 days ago - Pushed at: 9 days ago - Stars: 57 - Forks: 14
madvorak/duality
Duality theory in linear optimization and its extensions
Language: Lean - Size: 15.9 MB - Last synced at: 9 days ago - Pushed at: 9 days ago - Stars: 6 - Forks: 0
Seasawher/import-all
This script can check and auto-generate `import` statements in a lean4 repository.
Language: Lean - Size: 25.4 KB - Last synced at: 6 days ago - Pushed at: 9 days ago - Stars: 5 - Forks: 0
0art0/kimina
A Lean tactic that invokes the Kimina Prover Preview model to offer proof suggestions.
Language: Lean - Size: 43 KB - Last synced at: 9 days ago - Pushed at: 10 days ago - Stars: 7 - Forks: 0
dwrensha/tryAtEachStep
Try a tactic at each step in a Lean proof.
Language: Lean - Size: 146 KB - Last synced at: 10 days ago - Pushed at: 10 days ago - Stars: 25 - Forks: 3
lenianiva/Pantograph
(Mirror) A Machine-to-Machine Interaction System for Lean 4
Language: Lean - Size: 956 KB - Last synced at: 5 days ago - Pushed at: 9 days ago - Stars: 20 - Forks: 3
leanprover-community/import-graph
Tool to analyse the import structure of lean projects.
Language: Lean - Size: 292 KB - Last synced at: 10 days ago - Pushed at: 10 days ago - Stars: 11 - Forks: 10
leanprover/doc-gen4
Document Generator for Lean 4
Language: Lean - Size: 836 KB - Last synced at: 10 days ago - Pushed at: 10 days ago - Stars: 88 - Forks: 43
GrahamStrickland/mechanics_of_proof
My own implementation of the exercises and examples in "The Mechanics of Proof" - Heather Macbeth
Language: Lean - Size: 28.3 KB - Last synced at: 10 days ago - Pushed at: 10 days ago - Stars: 0 - Forks: 0
leanprover-community/quote4
Intuitive, type-safe expression quotations for Lean 4.
Language: Lean - Size: 227 KB - Last synced at: 10 days ago - Pushed at: 10 days ago - Stars: 83 - Forks: 14
lean-dojo/LeanDojo
Tool for data extraction and interacting with Lean programmatically.
Language: Python - Size: 2.23 MB - Last synced at: 10 days ago - Pushed at: 26 days ago - Stars: 657 - Forks: 103
gdncc/Cryptography
Lean 4 programming language and theorem prover cryptography experiments
Language: Lean - Size: 4.63 MB - Last synced at: 11 days ago - Pushed at: 11 days ago - Stars: 9 - Forks: 0
lean-dojo/LeanCopilot
LLMs as Copilots for Theorem Proving in Lean
Language: C++ - Size: 1.21 MB - Last synced at: 10 days ago - Pushed at: 10 days ago - Stars: 1,084 - Forks: 99
tbmreza/consig
Lean lib for signals simulations. Easy FFI with Python & Octave to keep our formality in check.
Language: Lean - Size: 110 KB - Last synced at: 11 days ago - Pushed at: 11 days ago - Stars: 0 - Forks: 0
a2435191/lean-logic-formalization
Formalize "Logic Notes" by Lou van den Dries in Lean
Language: Lean - Size: 32.2 KB - Last synced at: 11 days ago - Pushed at: 11 days ago - Stars: 11 - Forks: 0
Verified-zkEVM/ArkLib
Formally Verified Arguments of Knowledge in Lean
Language: Lean - Size: 2.95 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 67 - Forks: 10
GasStationManager/LeanTool
A "code intepreter" for Lean
Language: Python - Size: 126 KB - Last synced at: 11 days ago - Pushed at: 11 days ago - Stars: 29 - Forks: 2
hhu-adam/Robo
A game for learning lean 4 where a cute little Robo joins you on your exploration of the Mathiverse. The game is in German 🇩🇪
Language: Lean - Size: 235 MB - Last synced at: 11 days ago - Pushed at: 11 days ago - Stars: 21 - Forks: 13
rami3l/PLFaLean
Learn Lean 4 with PLFA proofs.
Language: Lean - Size: 256 KB - Last synced at: 9 days ago - Pushed at: about 1 month ago - Stars: 70 - Forks: 7
argumentcomputer/Blake3.lean
Lean4 bindings to Blake3
Language: Lean - Size: 88.9 KB - Last synced at: 12 days ago - Pushed at: 12 days ago - Stars: 5 - Forks: 1
dwrensha/animate-lean-proofs
tool for turning Lean proofs into Blender animations
Language: Lean - Size: 1.9 MB - Last synced at: about 20 hours ago - Pushed at: 12 days ago - Stars: 66 - Forks: 4
Hagb/lean-groebner 📦
Lean4 formalization of Gröbner basis (WIP)
Language: Lean - Size: 164 KB - Last synced at: 13 days ago - Pushed at: 13 days ago - Stars: 6 - Forks: 1
leanprover-community/duper
Language: Lean - Size: 1.7 MB - Last synced at: 9 days ago - Pushed at: 9 days ago - Stars: 69 - Forks: 11
mrigankpawagi/LeanearTemporalLogic
Formalization of Linear Temporal Logic (LTL) in Lean 4.
Language: Lean - Size: 167 KB - Last synced at: 13 days ago - Pushed at: 13 days ago - Stars: 1 - Forks: 0
KislyjKisel/Raylib.lean
Raylib bindings for Lean4
Language: Lean - Size: 792 KB - Last synced at: 13 days ago - Pushed at: 13 days ago - Stars: 24 - Forks: 3
leanprover/lean4-cli
A Lean 4 library for configuring Command Line Interfaces and parsing command line arguments.
Language: Lean - Size: 130 KB - Last synced at: 13 days ago - Pushed at: 13 days ago - Stars: 75 - Forks: 16
oembo-sse/gcl-lean
Lean formalization of GCL and parts of Formal Methods
Language: Lean - Size: 28.3 KB - Last synced at: 13 days ago - Pushed at: 13 days ago - Stars: 0 - Forks: 0
tristan-f-r/unsolved-lean
catalogue of sorrys or proof_wanted in established lean formalization projects.
Language: TypeScript - Size: 115 KB - Last synced at: 14 days ago - Pushed at: 14 days ago - Stars: 2 - Forks: 0
KislyjKisel/lean-pod
Low level utils (single precision float, byte spans, unboxed vector, finalization callbacks, fixnums, deque, slotmap etc; implemented via ffi)
Language: C - Size: 179 KB - Last synced at: 14 days ago - Pushed at: 14 days ago - Stars: 5 - Forks: 0
Danelnov/Lambda-Calculus-Formalization-
This formalization uses the De Bruijn indices, the objective is to formalize the Church-Rosser theorem
Language: Lean - Size: 2.93 KB - Last synced at: 15 days ago - Pushed at: 15 days ago - Stars: 0 - Forks: 0
Julian/rpylean
A Lean (4) type checker written in RPython
Language: Python - Size: 2.4 MB - Last synced at: 5 days ago - Pushed at: 15 days ago - Stars: 2 - Forks: 1
formalmind/formal-agent
Agents for formal verification
Language: Python - Size: 68.4 KB - Last synced at: 17 days ago - Pushed at: 17 days ago - Stars: 0 - Forks: 0
runtimeverification/evm-equivalence
Equivalence proofs of EVM models
Language: Lean - Size: 135 KB - Last synced at: 11 days ago - Pushed at: 11 days ago - Stars: 2 - Forks: 0
shnarazk/lucr
LaTeX math commands to Unicode symbols Converter in Rust
Language: Rust - Size: 32.2 KB - Last synced at: 18 days ago - Pushed at: 18 days ago - Stars: 0 - Forks: 0
aurora-dtu/theory
Collection of Lean 4 formalizations
Language: Lean - Size: 396 KB - Last synced at: 18 days ago - Pushed at: 18 days ago - Stars: 0 - Forks: 0
ionathanch/MutualInduction
An experimental mutual induction tactic for Lean 4.
Language: Lean - Size: 178 KB - Last synced at: 5 days ago - Pushed at: 19 days ago - Stars: 8 - Forks: 0
shnarazk/zed-lean4
Zed extension to support Lean4 language
Language: Scheme - Size: 759 KB - Last synced at: 19 days ago - Pushed at: 19 days ago - Stars: 2 - Forks: 0
anqur/TinyLean
Tiny theorem prover with syntax like Lean 4 in <1K LOC
Language: Python - Size: 285 KB - Last synced at: 10 days ago - Pushed at: 27 days ago - Stars: 25 - Forks: 0
lean-dojo/LeanDojoChatGPT
ChatGPT plugin for theorem proving in Lean
Language: Python - Size: 344 KB - Last synced at: 21 days ago - Pushed at: about 1 year ago - Stars: 118 - Forks: 14
mrigankpawagi/simpleafier
Command line tool to help improve the quality of Lean code by converting any "simp" to "simp only".
Language: Python - Size: 17.6 KB - Last synced at: 23 days ago - Pushed at: 23 days ago - Stars: 0 - Forks: 0