Skip to content

@Lean-zh Lean 中文文档翻译

Change the repository type filter

All

    Repositories list

    20 repositories

    • lean-zh.github.io

      Public
      Homepage of the Lean-zh website.
      MIT License
      •1•14•1•1•Updated Jan 3, 2025Jan 3, 2025

    • math-in-lean-source

      Public
      Source code for the Mathematics in Lean tutorial.
      Lean
      •71•3•0•0•Updated Dec 29, 2024Dec 29, 2024

    • lean4web

      Public
      The Lean 4 web editor
      TypeScript
      •
      Apache License 2.0
      •22•0•0•0•Updated Dec 28, 2024Dec 28, 2024

    • PyPantograph

      Public
      A Machine-to-Machine Interaction System for Lean 4.
      TeX
      •
      Apache License 2.0
      •8•0•0•1•Updated Dec 21, 2024Dec 21, 2024

    • tp-lean-zh

      Public
      Lean 定理证明
      JavaScript
      •
      Apache License 2.0
      •5•11•3•0•Updated Dec 4, 2024Dec 4, 2024

    • LeanDojo

      Public
      Tool for data extraction and interacting with Lean programmatically.
      Python
      •
      MIT License
      •94•2•0•0•Updated Dec 3, 2024Dec 3, 2024

    • math-in-lean-zh

      Public
      The user home repository for the Mathematics in Lean tutorial.
      HTML
      •197•6•13•1•Updated Nov 16, 2024Nov 16, 2024

    • mp-lean-zh

      Public
      Lean 4 元编程
      Lean
      •
      Apache License 2.0
      •56•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

    • GlimpseOfLean

      Public
      Lean 定理证明初探
      Lean
      •
      Apache License 2.0
      •56•3•1•0•Updated Oct 16, 2024Oct 16, 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

    • .github

      Public
      Public profile of Lean-zh
      MIT License
      •0•0•0•0•Updated Sep 10, 2024Sep 10, 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
      •6•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
      •10•26•14•0•Updated Jul 24, 2024Jul 24, 2024

    • lean4game

      Public
      Server to host lean games.
      TypeScript
      •
      GNU General Public License v3.0
      •38•0•0•0•Updated Jul 10, 2024Jul 10, 2024

    • lean4

      Public
      用作文档目的
      Lean
      •
      Apache License 2.0
      •439•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