Repositories list

• lean-zh.github.io

  Public
  Homepage of the Lean-zh website.

  MIT License

  •1•21•1•0•Updated Mar 21, 2025Mar 21, 2025

• repl

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

  Lean

  •38•0•0•0•Updated Mar 13, 2025Mar 13, 2025

• lean4web

  Public
  The Lean 4 web editor

  TypeScript

  •

  Apache License 2.0

  •31•0•0•0•Updated Mar 10, 2025Mar 10, 2025

• math-in-lean-zh

  Public
  Lean 形式化数学

  HTML

  •222•9•13•1•Updated Mar 3, 2025Mar 3, 2025

• GlimpseOfLean

  Public
  Lean 定理证明初探

  Lean

  •

  Apache License 2.0

  •65•4•1•0•Updated Mar 3, 2025Mar 3, 2025

• jixia_py

  Public
  Python binding of jixia

  Python

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

• .github

  Public
  Public profile of Lean-zh

  MIT License

  •0•0•0•0•Updated Feb 26, 2025Feb 26, 2025

• MyTactics

  Public
  Demo Project

  Lean

  •0•0•0•0•Updated Feb 14, 2025Feb 14, 2025

• LoVe2025-zh

  Public
  《逻辑验证漫游指南》（2025 版）及相关材料

  Lean

  •4•0•15•1•Updated Jan 15, 2025Jan 15, 2025

• PyPantograph

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

  TeX

  •

  Apache License 2.0

  •15•0•0•0•Updated Jan 13, 2025Jan 13, 2025

• math-in-lean-source

  Public
  Source code for the Mathematics in Lean tutorial.

  Lean

  •77•3•0•0•Updated Dec 29, 2024Dec 29, 2024

• tp-lean-zh

  Public
  Lean 定理证明

  JavaScript

  •

  Apache License 2.0

  •7•13•3•0•Updated Dec 4, 2024Dec 4, 2024

• LeanDojo

  Public
  Tool for data extraction and interacting with Lean programmatically.

  Python

  •

  MIT License

  •98•2•0•0•Updated Dec 3, 2024Dec 3, 2024

• mp-lean-zh

  Public
  Lean 4 元编程

  Lean

  •

  Apache License 2.0

  •62•5•0•0•Updated Oct 29, 2024Oct 29, 2024

• IMO_2024

  Public
  Lean Solution to IMO 2024.

  Lean

  •0•1•0•0•Updated Oct 21, 2024Oct 21, 2024

• HTPIwL

  Public
  Book about using Lean with How To Prove It

  TeX

  •

  Creative Commons Attribution Share Alike 4.0 International

  •5•0•1•1•Updated Sep 23, 2024Sep 23, 2024

• IMO_Resource

  Public
  Resource of IMO(International Mathematical Olympiad)

  Jupyter Notebook

  •

  MIT License

  •1•2•0•0•Updated Sep 10, 2024Sep 10, 2024

• type_checking_in_lean4

  Public
  Type Checking in Lean 4

  JavaScript

  •

  Apache License 2.0

  •7•1•0•0•Updated Sep 1, 2024Sep 1, 2024

• GlimpseToGame

  Public
  A Game Adaptation of the document GlimpseOfLean.

  Lean

  •

  MIT License

  •0•0•0•1•Updated Aug 17, 2024Aug 17, 2024

• fp-lean-zh

  Public
  Lean 函数式编程

  JavaScript

  •

  Other

  •11•27•14•0•Updated Jul 24, 2024Jul 24, 2024

• lean4game

  Public
  Server to host lean games.

  TypeScript

  •

  GNU General Public License v3.0

  •43•0•0•0•Updated Jul 10, 2024Jul 10, 2024

• lean4

  Public
  用作文档目的

  Lean

  •

  Apache License 2.0

  •551•0•0•0•Updated Jun 29, 2024Jun 29, 2024

• flypitch

  Public
  A formal proof of the independence of the continuum hypothesis

  Lean

  •

  Apache License 2.0

  •15•0•0•0•Updated Jan 13, 2022Jan 13, 2022

• formalabstracts

  Public
  Lean

  •

  MIT License

  •43•0•0•0•Updated Nov 5, 2019Nov 5, 2019