Skip to content

@leanprover Lean

Change the repository type filter

All

    Repositories list

    71 repositories

    • lean4

      Public
      Lean 4 programming language and theorem prover
      leanlean4
      Lean
      •
      Apache License 2.0
      •659•6.4k•749•317•Updated Sep 15, 2025Sep 15, 2025

    • reference-manual

      Public
      The Lean reference manual
      Lean
      •
      Apache License 2.0
      •38•80•90•9•Updated Sep 15, 2025Sep 15, 2025

    • lean4-pr-releases

      Public
      Automated releases from leanprover/lean4 PRs
      3•2•0•0•Updated Sep 15, 2025Sep 15, 2025

    • KLR

      Public
      A formalization of ML kernel languages
      C
      •
      Apache License 2.0
      •7•26•6•5•Updated Sep 15, 2025Sep 15, 2025

    • verso

      Public
      Lean documentation authoring tool
      JavaScript
      •
      Apache License 2.0
      •95•217•45•6•Updated Sep 15, 2025Sep 15, 2025

    • Pantograph

      Public
      (Mirror) A Machine-to-Machine Interaction System for Lean 4
      machine-learningtheorem-provingproof-assistantlean4
      Lean
      •
      Apache License 2.0
      •4•32•0•0•Updated Sep 15, 2025Sep 15, 2025

    • radar

      Public
      Java
      •0•0•0•0•Updated Sep 15, 2025Sep 15, 2025

    • cslib

      Public
      A Lean library for Computer Science
      computer-sciencelean
      Lean
      •
      Apache License 2.0
      •20•113•2•7•Updated Sep 15, 2025Sep 15, 2025

    • subverso

      Public
      Lean
      •
      Apache License 2.0
      •6•6•4•0•Updated Sep 15, 2025Sep 15, 2025

    • vscode-lean4

      Public
      Visual Studio Code extension for the Lean 4 proof assistant
      leanvscode
      TypeScript
      •
      Apache License 2.0
      •76•226•54•10•Updated Sep 15, 2025Sep 15, 2025

    • human-eval-lean

      Public
      Hand-written verified Lean solutions for the HumanEval benchmark
      Lean
      •
      MIT License
      •6•19•154•6•Updated Sep 15, 2025Sep 15, 2025

    • lean4-nightly

      Public
      Nightly builds
      3•22•0•1•Updated Sep 15, 2025Sep 15, 2025

    • doc-gen4

      Public
      Document Generator for Lean 4
      lean4
      Lean
      •
      Apache License 2.0
      •52•103•23•0•Updated Sep 15, 2025Sep 15, 2025

    • lean4checker

      Public
      Replay the `Environment` for a given Lean module, ensuring that all declarations are accepted by the kernel.
      Lean
      •
      Apache License 2.0
      •9•26•0•1•Updated Sep 15, 2025Sep 15, 2025

    • lean4-cli

      Public
      A Lean 4 library for configuring Command Line Interfaces and parsing command line arguments.
      clileanlean4
      Lean
      •
      MIT License
      •19•83•1•0•Updated Sep 15, 2025Sep 15, 2025

    • reservoir-index

      Public
      Registry index for Reservoir
      Lean
      •2•5•0•0•Updated Sep 14, 2025Sep 14, 2025

    • reservoir

      Public
      Package registry for Lean/Lake.
      Vue
      •
      Apache License 2.0
      •6•24•13•3•Updated Sep 13, 2025Sep 13, 2025

    • adt

      Public
      Lean
      •
      Apache License 2.0
      •0•0•0•0•Updated Sep 12, 2025Sep 12, 2025

    • LeroyCompilerVerificationCourse

      Public
      Lean
      •
      GNU Lesser General Public License v2.1
      •2•6•0•0•Updated Sep 11, 2025Sep 11, 2025

    • theorem_proving_in_lean4

      Public
      Theorem Proving in Lean 4
      leanlean4
      Lean
      •
      Apache License 2.0
      •104•206•45•18•Updated Sep 10, 2025Sep 10, 2025

    • fp-lean

      Public
      Functional Programming in Lean
      Lean
      •
      Other
      •48•109•45•4•Updated Sep 10, 2025Sep 10, 2025

    • lean-action

      Public
      GitHub action for standard CI in Lean projects
      leangithub-actionslean4
      Shell
      •
      Apache License 2.0
      •9•22•8•1•Updated Sep 7, 2025Sep 7, 2025

    • velcom

      Public
      Continuous benchmarking
      Java
      •
      MIT License
      •1•19•4•0•Updated Sep 4, 2025Sep 4, 2025

    • verso-templates

      Public
      Templates for getting started with Verso
      Lean
      •1•0•0•1•Updated Aug 18, 2025Aug 18, 2025

    • TensorLib

      Public
      A verified tensor library in Lean
      Lean
      •
      Apache License 2.0
      •6•29•2•1•Updated Aug 15, 2025Aug 15, 2025

    • LNSym

      Public
      Armv8 Native Code Symbolic Simulator in Lean
      lean4
      Lean
      •
      Apache License 2.0
      •22•84•7•14•Updated Aug 12, 2025Aug 12, 2025

    • vetss2025

      Public
      Lean
      •1•1•0•0•Updated Aug 12, 2025Aug 12, 2025

    • SHerLOC

      Public
      A StableHLO analyzer in Lean
      Lean
      •
      Apache License 2.0
      •3•18•1•0•Updated Jul 22, 2025Jul 22, 2025

    • lean4-api-docs

      Public
      doc-gen4-based api documentation for lean
      1•2•0•0•Updated Jun 26, 2025Jun 26, 2025

    • lean4export

      Public
      Plain-text declaration export for Lean 4
      Lean
      •
      Apache License 2.0
      •11•19•2•1•Updated Jun 6, 2025Jun 6, 2025