The following is an incomplete list of Lean 4 projects:
- 0art0/CategoryTheory
- Anderssorby/LeanPlay
- Augustindou/natural2lean
- Augustindou/natural2lean-lean-project-template
- AwdeDarkar/my-mathlib
- FWuermse/lean-postgres
- FWuermse/lean4-sql-utils
- Ferinko/LeanAStar
- Ferinko/LeanSha
- GregorKikelj/Lean4AdventOfCode
- IPDSnelting/tba-2022
- Izzimach/lean-glfw
- Izzimach/qinglong
- JLimperg/aesop
- JamesGallicchio/LeanColls
- Julian/lean.nvim
- Kha/do-supplement
- Kha/lean4-nightly
- Kha/nale
- Mateiadrielrafael/lean-sandbox
- NicolasRouquette/dimensional-calculus.lean4
- Nolrai/WildGeo
- Nolrai/pharoh
- PeterKementzey/graph-library-for-lean4
- PolyB/LeanPythonRaw
- RosieBaish/first_order_leaning
- RosieBaish/lean-sep-logic
- SReichelt/universe-abstractions
- SnO2WMaN/lean-first-practice
- Vtec234/lean-sat
- Vtec234/npm-widget
- WinstonHartnett/lean-club
- abentkamp/duper
- adamtopaz/lean4_advent_2021
- agentultra/LeanParsec
- agentultra/lean-4-hackers
- alcides/untyped
- alecvv/proof-mining.preview
- alexkeizer/qpf4
- ammkrn/JohnDoe
- ammkrn/UsCourts
- ammkrn/prolala_demo
- ammkrn/timelib
- arademaker/mrs
- arthurpaulino/FxyLang
- arthurpaulino/LeanMusic
- arthurpaulino/LeanMySQL
- arthurpaulino/LeanREPL
- arthurpaulino/NumLean
- arthurpaulino/lean4-metaprogramming-book
- avigad/lamr
- bollu/lean-to
- bollu/lean4_docs
- chasenorman/FormalizedFoundations
- cipher1024/lean4-prog
- crabbo-rave/Soup
- crabbo-rave/lean4-Hangman
- crabbo-rave/lean4-Tuple
- crabbo-rave/useless_macros
- cristinaborza/Logic-in-Lean
- cristinaborza/S5
- cruhland/lean4-analysis
- cruhland/lean4-axiomatic
- emap-ic/syllabus
- felipegchi/books
- felipegchi/lyre
- fgdorais/GMLAlgebra
- fgdorais/GMLInit
- forked-from-1kasper/lean-vcpu
- g4rgoil/tba-project
- gabriel-fallen/bidirectional-demo
- gebner/oleanparser
- gebner/quote4
- hargoniX/cpdt-lean
- hargoniX/lean-ink-bug
- hargoniX/lean4-c-bug
- hargoniX/lean4-fixed
- hargoniX/lean4-statvfs
- hcheval/ProofMiningLean
- insightmind/LeanInk
- intsuc/unified-bidirectional-elaboration
- javra/iit
- jessetvogel/duck
- joehendrix/lean-arith-solver
- joehendrix/lean-crypto
- joehendrix/lean-sat-checker
- justinfargnoli/koi
- langfield/mergesort
- langfield/nflow
- larsk21/iris-lean
- leanprover-community/lean3port
- leanprover-community/mathlib3port
- leanprover-community/mathlib4
- leanprover-community/mathport
- leanprover-community/test-mathport
- leanprover/LeanInk
- leanprover/doc-gen4
- leanprover/lake
- leanprover/lean4
- leanprover/lean4-samples
- leanprover/vscode-lean4
- lecopivo/EigenLean
- lecopivo/HouLean
- lecopivo/SciLean
- lecopivo/lean4-karray
- lecopivo/leanPluginTest
- marcusrossel/model-checking
- marcusrossel/reactor-model
- mhuisi/lean4-cli
- opencompl/lean-gap
- opencompl/lean-mlir
- opencompl/lean-mlir-semantics
- pnwamk/lean4-assert-command
- ramonfmir/junglean
- rebryant/model-counting
- remimimimimi/lambda-calculus-typecheckers
- remimimimimi/lean4-type-theory
- shingtaklam1324/iva
- siddhartha-gadgil/Polylean
- siddhartha-gadgil/Saturn
- siddhartha-gadgil/lean-loris
- siddhartha-gadgil/lean4-scratch
- technosentience/ltlcheck
- tydeu/folktale
- tydeu/lean4-alloy
- tydeu/lean4-itertools
- tylerhanks/AwodeyCT
- ufmg-smite/lean-smt
- user7230724/lean-projects4
- xubaiw/BaseN.lean
- xubaiw/CMark.lean
- xubaiw/Dirs.lean
- xubaiw/Dta.lean
- xubaiw/Economics.lean
- xubaiw/Reservoir.lean
- xubaiw/Socket.lean
- xubaiw/Unicode.lean
- xubaiw/WaterSortPuzzle.lean
- xubaiw/csv
- xubaiw/lean-problem-dynamic-link
- xubaiw/lean4-terminal
- xubaiw/sjtu-math2501-ode
- yatima-inc/Http.lean
- yatima-inc/LSpec
- yatima-inc/Megaparsec.lean
- yatima-inc/Radiya.lean
- yatima-inc/Spark.lean
- yatima-inc/yatima-lang
- zaxioms/LeanAlg
- zenna/LeanOmega
- zygi/lean4-sha3