Repositories list

• mathlib4

  Public
  The math library of Lean 4

  lean4

  Lean

  •

  Apache License 2.0

  •375•1.8k•237•1.3k•Updated Mar 1, 2025Mar 1, 2025

• flt-regular

  Public
  Fermat's Last Theorem for regular primes

  Lean

  •

  Apache License 2.0

  •3•52•0•0•Updated Mar 1, 2025Mar 1, 2025

• batteries

  Public
  The "batteries included" extended library for the Lean programming language and theorem prover

  leanlean4

  Lean

  •

  Apache License 2.0

  •116•284•21•54•Updated Mar 1, 2025Mar 1, 2025

• leanprover-community.github.io

  Public
  Hosts the website for mathlib and other Lean community infrastructure.

  CSS

  •

  MIT License

  •134•58•21•10•Updated Mar 1, 2025Mar 1, 2025

• mathlib_stats

  Public
  Display gitstats output on the mathlib website

  Python

  •6•1•0•0•Updated Mar 1, 2025Mar 1, 2025

• lean4-metaprogramming-book

  Public
  lean4

  Lean

  •

  Apache License 2.0

  •61•236•16•8•Updated Feb 28, 2025Feb 28, 2025

• aesop

  Public
  White-box automation for Lean 4

  lean4

  Lean

  •

  Apache License 2.0

  •30•240•28•1•Updated Feb 28, 2025Feb 28, 2025

• blog

  Public
  Source for the community blog

  Python

  •21•6•4•8•Updated Feb 28, 2025Feb 28, 2025

• lean4game

  Public
  Server to host lean games.

  reactlean4

  TypeScript

  •

  GNU General Public License v3.0

  •42•237•87•6•Updated Feb 27, 2025Feb 27, 2025

• quote4

  Public
  Intuitive, type-safe expression quotations for Lean 4.

  lean4

  Lean

  •

  Apache License 2.0

  •13•79•13•5•Updated Feb 25, 2025Feb 25, 2025

• duper

  Public
  lean4

  Lean

  •

  Apache License 2.0

  •10•63•0•0•Updated Feb 25, 2025Feb 25, 2025

• lean-auto

  Public
  Experiments in automation for Lean

  Lean

  •

  Apache License 2.0

  •16•93•7•0•Updated Feb 25, 2025Feb 25, 2025

• lean4web

  Public
  The Lean 4 web editor

  lean4

  TypeScript

  •

  Apache License 2.0

  •26•82•7•0•Updated Feb 25, 2025Feb 25, 2025

• ProofWidgets4

  Public
  Helper toolkit for creating your own Lean 4 UserWidgets

  leanlean4visualization

  Lean

  •

  Apache License 2.0

  •32•126•14•0•Updated Feb 23, 2025Feb 23, 2025

• mathematics_in_lean

  Public
  The user home repository for the Mathematics in Lean tutorial.

  HTML

  •214•303•0•0•Updated Feb 21, 2025Feb 21, 2025

• iris-lean

  Public
  Lean 4 port of Iris, a higher-order concurrent separation logic framework

  Lean

  •

  Apache License 2.0

  •9•83•3•1•Updated Feb 20, 2025Feb 20, 2025

• sphere-eversion

  Public
  Formalization of the existence of sphere eversions

  Lean

  •

  Apache License 2.0

  •13•38•0•0•Updated Feb 17, 2025Feb 17, 2025

• logic_and_proof

  Public
  TeX

  •

  Apache License 2.0

  •2•8•0•0•Updated Feb 17, 2025Feb 17, 2025

• import-graph

  Public
  Tool to analyse the import structure of lean projects.

  lean4

  Lean

  •

  Apache License 2.0

  •10•9•3•1•Updated Feb 17, 2025Feb 17, 2025

• NNG4

  Public
  Natural Number Game

  lean4

  Lean

  •

  Apache License 2.0

  •40•149•20•2•Updated Feb 17, 2025Feb 17, 2025

• mathlib4_docs

  Public
  lean4

  3•8•0•0•Updated Feb 16, 2025Feb 16, 2025

• azure-scripts

  Public
  scripts and cron jobs for Azure

  Python

  •5•1•0•0•Updated Feb 14, 2025Feb 14, 2025

• mathlib-manual

  Public
  JavaScript

  •

  Apache License 2.0

  •13•0•0•0•Updated Feb 11, 2025Feb 11, 2025

• LeanSearchClient

  Public
  Syntax for searching with natural language from Lean, using https://leansearch.net/ (may extend to other services)

  Lean

  •

  Apache License 2.0

  •3•14•1•0•Updated Feb 10, 2025Feb 10, 2025

• repl

  Public
  A simple REPL for Lean 4, returning information about errors and sorries.

  Lean

  •36•103•13•4•Updated Feb 4, 2025Feb 4, 2025

• plausible

  Public
  Lean

  •

  Apache License 2.0

  •4•30•1•2•Updated Feb 3, 2025Feb 3, 2025

• lean4-mode

  Public
  Emacs major mode for Lean 4

  emacslean4

  Emacs Lisp

  •

  Apache License 2.0

  •32•80•19•3•Updated Jan 17, 2025Jan 17, 2025

• con-nf

  Public
  A formal consistency proof of Quine's set theory New Foundations

  set-theorylean4new-foundations

  Lean

  •

  Apache License 2.0

  •7•67•1•0•Updated Jan 8, 2025Jan 8, 2025

• mathport

  Public
  Mathport is a tool for porting Lean3 projects to Lean4

  Lean

  •

  Apache License 2.0

  •15•43•33•4•Updated Nov 21, 2024Nov 21, 2024

• doc-gen

  Public
  Generate HTML documentation for mathlib and Lean

  documentation-generator

  Python

  •

  Apache License 2.0

  •20•21•23•9•Updated Sep 28, 2024Sep 28, 2024