Repositories list

• lean4

  Public
  Lean 4 programming language and theorem prover

  leanlean4

  leanlean4

  Lean

  •

  Apache License 2.0

  •930930 forks•8.8k8.8k stars•965965 issues•634634 pull requests•Updated Aug 11, 2026Aug 11, 2026

• lean4-pr-releases

  Public
  Automated releases from leanprover/lean4 PRs

  33 forks•33 stars•00 issues•00 pull requests•Updated Aug 11, 2026Aug 11, 2026

• downstream-lean4

  Public
  A collection of packages downstream of Lean 4.

  Lean

  •11 fork•11 star•00 issues•55 pull requests•Updated Aug 11, 2026Aug 11, 2026

• verso

  Public
  Lean documentation authoring tool

  Lean

  •

  Apache License 2.0

  •119119 forks•373373 stars•6464 issues•1717 pull requests•Updated Aug 11, 2026Aug 11, 2026

• reference-manual

  Public
  The Lean reference manual

  Lean

  •

  Apache License 2.0

  •6363 forks•122122 stars•113113 issues•1818 pull requests•Updated Aug 11, 2026Aug 11, 2026

• lean-kernel-arena

  Public
  Lean

  •2121 forks•3232 stars•00 issues•00 pull requests•Updated Aug 11, 2026Aug 11, 2026

• lean4-nightly

  Public
  Nightly builds

  33 forks•2323 stars•00 issues•00 pull requests•Updated Aug 11, 2026Aug 11, 2026

• lean4export

  Public
  Plain-text declaration export for Lean 4

  Lean

  •

  Apache License 2.0

  •2222 forks•3838 stars•22 issues•11 pull request•Updated Aug 11, 2026Aug 11, 2026

• comparator

  Public
  Lean

  •

  Apache License 2.0

  •2121 forks•134134 stars•77 issues•66 pull requests•Updated Aug 11, 2026Aug 11, 2026

• cslib

  Public
  The Lean Computer Science Library (CSLib)

  computer-sciencelean

  computer-sciencelean

  Lean

  •

  Apache License 2.0

  •179179 forks•644644 stars•4747 issues•9898 pull requests•Updated Aug 11, 2026Aug 11, 2026

• hex-berlekamp-zassenhaus-mathlib

  Public
  Mathlib proofs for Hex Berlekamp-Zassenhaus factorization

  Lean

  •

  Apache License 2.0

  •00 forks•00 stars•00 issues•00 pull requests•Updated Aug 11, 2026Aug 11, 2026

• hex-berlekamp-zassenhaus

  Public
  Verified Berlekamp-Zassenhaus factorization over the integers

  Lean

  •

  Apache License 2.0

  •00 forks•00 stars•00 issues•00 pull requests•Updated Aug 11, 2026Aug 11, 2026

• hex-berlekamp-mathlib

  Public
  Mathlib proofs for Hex Berlekamp factorization

  Lean

  •

  Apache License 2.0

  •00 forks•00 stars•00 issues•00 pull requests•Updated Aug 11, 2026Aug 11, 2026

• hex-berlekamp

  Public
  Verified Berlekamp factorization over finite fields

  Lean

  •

  Apache License 2.0

  •00 forks•00 stars•00 issues•00 pull requests•Updated Aug 11, 2026Aug 11, 2026

• verso-templates

  Public
  Templates for getting started with Verso

  Lean

  •44 forks•3737 stars•33 issues•11 pull request•Updated Aug 11, 2026Aug 11, 2026

• verso-slides

  Public
  Lean

  •

  Apache License 2.0

  •33 forks•1616 stars•1010 issues•00 pull requests•Updated Aug 11, 2026Aug 11, 2026

• verso-web-components

  Public
  A collection of reusable components from the Lean website designed build related sites with the same look and feel.

  Lean

  •

  Apache License 2.0

  •00 forks•33 stars•00 issues•11 pull request•Updated Aug 11, 2026Aug 11, 2026

• hex

  Public
  Verified computational algebra in Lean 4: aggregator for the released hex libraries

  Lean

  •

  Apache License 2.0

  •22 forks•1515 stars•00 issues•00 pull requests•Updated Aug 11, 2026Aug 11, 2026

• lean-action

  Public
  GitHub action for standard CI in Lean projects

  leangithub-actionslean4

  leangithub-actionslean4

  Shell

  •

  Apache License 2.0

  •2121 forks•3939 stars•1313 issues•1717 pull requests•Updated Aug 11, 2026Aug 11, 2026

• radar-bench-verso

  Public
  Radar benchmarking for verso

  Python

  •00 forks•00 stars•00 issues•22 pull requests•Updated Aug 11, 2026Aug 11, 2026

• nerodia

  Public
  Write Python modules in Lean! (WIP)

  Lean

  •

  Apache License 2.0

  •00 forks•33 stars•00 issues•00 pull requests•Updated Aug 11, 2026Aug 11, 2026

• lean-workbench

  Public
  Online Lean Workbench

  TypeScript

  •

  Apache License 2.0

  •00 forks•44 stars•1818 issues•22 pull requests•Updated Aug 10, 2026Aug 10, 2026

• subverso

  Public
  Lean

  •

  Apache License 2.0

  •1313 forks•88 stars•33 issues•22 pull requests•Updated Aug 10, 2026Aug 10, 2026

• doc-gen4

  Public
  Document Generator for Lean 4

  lean4

  lean4

  Lean

  •

  Apache License 2.0

  •6767 forks•165165 stars•3131 issues•66 pull requests•Updated Aug 10, 2026Aug 10, 2026

• leansqlite

  Public
  SQLite bindings for Lean

  C

  •

  Apache License 2.0

  •11 fork•5252 stars•00 issues•00 pull requests•Updated Aug 10, 2026Aug 10, 2026

• illuminate

  Public
  Lean

  •

  Apache License 2.0

  •11 fork•1111 stars•00 issues•00 pull requests•Updated Aug 10, 2026Aug 10, 2026

• lean4-cli

  Public
  A Lean 4 library for configuring Command Line Interfaces and parsing command line arguments.

  clileanlean4

  clileanlean4

  Lean

  •

  MIT License

  •2828 forks•116116 stars•22 issues•44 pull requests•Updated Aug 10, 2026Aug 10, 2026

• lean-eval-submissions

  Public
  Submission pipeline and results store for the lean-eval benchmark (https://github.com/leanprover/lean-eval)

  Python

  •

  Apache License 2.0

  •11 fork•66 stars•11 issue•00 pull requests•Updated Aug 10, 2026Aug 10, 2026

• leagent

  Public
  Lean

  •00 forks•22 stars•00 issues•11 pull request•Updated Aug 10, 2026Aug 10, 2026

• downstream-lean4-fork-mathlib4

  Public
  A fork of mathlib4 used by downstream-lean4 to open PRs

  1.6k1.6k forks•00 stars•00 issues•00 pull requests•Updated Aug 10, 2026Aug 10, 2026