Repositories list

• reference-manual

  Public
  Lean 参考手册

  Lean

  •

  Apache License 2.0

  •6565 forks•11 star•11 issue•00 pull requests•Updated Aug 16, 2026Aug 16, 2026

• lean-zh.github.io

  Public
  Homepage of the Lean-zh website.

  MIT License

  •22 forks•5959 stars•11 issue•00 pull requests•Updated Aug 13, 2026Aug 13, 2026

• protobuf

  Public
  protobuf implementation for Lean 4

  protobufmetaprogramminglean4

  protobufmetaprogramminglean4

  Lean

  •

  MIT License

  •11 fork•99 stars•00 issues•00 pull requests•Updated Aug 3, 2026Aug 3, 2026

• binary

  Public
  Lean

  •

  MIT License

  •11 fork•44 stars•00 issues•00 pull requests•Updated Aug 3, 2026Aug 3, 2026

• lean-tactic-programming-guide-zh

  Public
  Beginner's guide to Tactic Programming in Lean

  Lean

  •

  Apache License 2.0

  •1010 forks•00 stars•00 issues•00 pull requests•Updated Aug 1, 2026Aug 1, 2026

• lean-metaprogramming-recipes-zh

  Public
  Lean 4（元）编程 Cookbook 中文版

  metaprogrammingtheorem-provingcookbook+ 2

  metaprogrammingtheorem-provingcookbookchinese-translationlean4

  Lean

  •

  MIT License

  •77 forks•00 stars•00 issues•00 pull requests•Updated Jul 31, 2026Jul 31, 2026

• LoVe-zh

  Public
  逻辑验证漫游指南

  Lean

  •55 forks•7474 stars•00 issues•11 pull request•Updated Jul 18, 2026Jul 18, 2026

• LeanUp

  Public
  Python

  •

  MIT License

  •11 fork•22 stars•00 issues•00 pull requests•Updated Jul 7, 2026Jul 7, 2026

• tp-lean-zh

  Public
  Lean 定理证明

  Lean

  •

  Apache License 2.0

  •1212 forks•2828 stars•44 issues•00 pull requests•Updated Jul 5, 2026Jul 5, 2026

• fp-lean-zh

  Public
  Lean 函数式编程

  Lean

  •

  Other

  •1515 forks•4545 stars•1515 issues•11 pull request•Updated Jul 3, 2026Jul 3, 2026

• lean4web

  Public
  The Lean 4 web editor

  TypeScript

  •

  Apache License 2.0

  •6262 forks•11 star•00 issues•00 pull requests•Updated Jun 30, 2026Jun 30, 2026

• HoTTLean

  Public
  Lean

  •

  Apache License 2.0

  •1616 forks•00 stars•00 issues•00 pull requests•Updated Jun 12, 2026Jun 12, 2026

• linear-algebra-done-right-lean

  Public
  Lean Companion to Axler's Linear Algebra Done Right

  Lean

  •88 forks•00 stars•00 issues•00 pull requests•Updated May 26, 2026May 26, 2026

• HTPIwL

  Public
  Book about using Lean with How To Prove It

  JavaScript

  •

  Creative Commons Attribution Share Alike 4.0 International

  •44 forks•00 stars•11 issue•00 pull requests•Updated May 13, 2026May 13, 2026

• logic_and_proof

  Public
  TeX

  •

  Apache License 2.0

  •88 forks•00 stars•00 issues•00 pull requests•Updated Apr 7, 2026Apr 7, 2026

• GlimpseToGame

  Public
  A Game Adaptation of the document GlimpseOfLean.

  Lean

  •

  MIT License

  •00 forks•00 stars•00 issues•11 pull request•Updated Mar 2, 2026Mar 2, 2026

• GlimpseOfLean

  Public
  Lean 定理证明初探

  Lean

  •

  Apache License 2.0

  •155155 forks•4444 stars•11 issue•00 pull requests•Updated Mar 1, 2026Mar 1, 2026

• SciLean

  Public
  Lean 4 科学计算

  Lean

  •

  Apache License 2.0

  •4242 forks•00 stars•00 issues•00 pull requests•Updated Feb 18, 2026Feb 18, 2026

• LinearAlgebraGame

  Public
  Python

  •

  MIT License

  •88 forks•00 stars•00 issues•00 pull requests•Updated Jan 26, 2026Jan 26, 2026

• math-in-lean-zh

  Public
  Lean 形式化数学

  HTML

  •408408 forks•1919 stars•1313 issues•00 pull requests•Updated Dec 20, 2025Dec 20, 2025

• lean4game

  Public
  Server to host lean games.

  TypeScript

  •

  GNU General Public License v3.0

  •9898 forks•11 star•00 issues•00 pull requests•Updated Oct 7, 2025Oct 7, 2025

• lean-explore

  Public
  A search engine for Lean 4 declarations

  Python

  •

  Apache License 2.0

  •1313 forks•00 stars•00 issues•00 pull requests•Updated Aug 9, 2025Aug 9, 2025

• repl

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

  Lean

  •

  Apache License 2.0

  •6868 forks•00 stars•00 issues•00 pull requests•Updated Jul 23, 2025Jul 23, 2025

• lean-docs-zh

  Public
  Chinese translation of the official Lean documentation.

  Python

  •

  MIT License

  •11 fork•44 stars•00 issues•00 pull requests•Updated Jun 30, 2025Jun 30, 2025

• type-checking-in-lean-zh

  Public
  Book about type checking in Lean (Simpilfied Chinese)

  JavaScript

  •

  Apache License 2.0

  •00 forks•11 star•00 issues•00 pull requests•Updated Jun 10, 2025Jun 10, 2025

• analysis

  Public
  A Lean companion to Analysis I

  Lean

  •

  Apache License 2.0

  •261261 forks•00 stars•00 issues•00 pull requests•Updated Jun 1, 2025Jun 1, 2025

• NeqMath

  Public
  Lean Repo from https://github.com/Lizn-zn/NeqLIPS

  Lean

  •00 forks•00 stars•00 issues•00 pull requests•Updated Apr 9, 2025Apr 9, 2025

• PyPantograph

  Public
  A Machine-to-Machine Interaction System for Lean 4.

  Python

  •

  Apache License 2.0

  •3535 forks•00 stars•00 issues•00 pull requests•Updated Apr 8, 2025Apr 8, 2025

• mp-lean-zh

  Public
  Lean 4 元编程

  Lean

  •

  Apache License 2.0

  •7777 forks•77 stars•00 issues•00 pull requests•Updated Apr 4, 2025Apr 4, 2025

• jixia_py

  Public
  Python binding of jixia

  Python

  •22 forks•00 stars•00 issues•00 pull requests•Updated Mar 1, 2025Mar 1, 2025