Skip to content

@leanprover Lean

Change the repository type filter

All

    Repositories list

    60 repositories

    • doc-gen4

      Public
      Document Generator for Lean 4
      lean4
      Lean
      •
      Apache License 2.0
      •42•71•22•1•Updated Dec 25, 2024Dec 25, 2024

    • reservoir-index

      Public
      Registry index for Reservoir
      Lean
      •1•2•0•0•Updated Dec 25, 2024Dec 25, 2024

    • lean4

      Public
      Lean 4 programming language and theorem prover
      leanlean4
      Lean
      •
      Apache License 2.0
      •437•4.9k•612•181•Updated Dec 25, 2024Dec 25, 2024

    • lean4-nightly

      Public
      Nightly builds
      3•22•0•1•Updated Dec 25, 2024Dec 25, 2024

    • lean4-pr-releases

      Public
      Automated releases from leanprover/lean4 PRs
      1•2•0•0•Updated Dec 24, 2024Dec 24, 2024

    • TensorLib

      Public
      A verified tensor library in Lean
      Lean
      •
      Apache License 2.0
      •0•16•0•0•Updated Dec 24, 2024Dec 24, 2024

    • NKL

      Public
      A formalization of the NKI ISA
      Python
      •
      Apache License 2.0
      •0•4•0•0•Updated Dec 23, 2024Dec 23, 2024

    • reference-manual

      Public
      JavaScript
      •
      Apache License 2.0
      •5•34•69•1•Updated Dec 22, 2024Dec 22, 2024

    • verso

      Public
      Lean documentation authoring tool
      Lean
      •
      Apache License 2.0
      •14•128•35•2•Updated Dec 22, 2024Dec 22, 2024

    • vscode-lean4

      Public
      Visual Studio Code extension for the Lean 4 proof assistant
      leanvscode
      TypeScript
      •
      Apache License 2.0
      •52•174•45•9•Updated Dec 18, 2024Dec 18, 2024

    • lean-llvm

      Public
      Custom-built LLVM toolchain for use in Lean 4
      5•6•0•1•Updated Dec 15, 2024Dec 15, 2024

    • elan

      Public
      The Lean version manager
      Rust
      •
      Apache License 2.0
      •37•328•26•2•Updated Dec 11, 2024Dec 11, 2024

    • LNSym

      Public
      Armv8 Native Code Symbolic Simulator in Lean
      lean4
      Lean
      •
      Apache License 2.0
      •18•66•7•13•Updated Dec 9, 2024Dec 9, 2024

    • subverso

      Public
      Lean
      •
      Apache License 2.0
      •2•4•4•0•Updated Dec 6, 2024Dec 6, 2024

    • lean4checker

      Public
      Replay the `Environment` for a given Lean module, ensuring that all declarations are accepted by the kernel.
      Lean
      •
      Apache License 2.0
      •6•18•0•2•Updated Dec 2, 2024Dec 2, 2024

    • lean-action

      Public
      GitHub action for standard CI in Lean projects
      leangithub-actionslean4
      Shell
      •
      Apache License 2.0
      •3•16•3•2•Updated Nov 28, 2024Nov 28, 2024

    • lean4-cli

      Public
      A Lean 4 library for configuring Command Line Interfaces and parsing command line arguments.
      clileanlean4
      Lean
      •
      MIT License
      •12•72•1•0•Updated Nov 5, 2024Nov 5, 2024

    • lean4wip

      Public
      Lean 4 fork for working in progress development
      Lean
      •
      Apache License 2.0
      •437•0•0•0•Updated Oct 31, 2024Oct 31, 2024

    • TenCert

      Public
      Verified tensor compilation in Lean
      Lean
      •
      Apache License 2.0
      •0•3•0•0•Updated Oct 29, 2024Oct 29, 2024

    • theorem_proving_in_lean

      Public
      Theorem proving in Lean
      Python
      •
      Apache License 2.0
      •47•48•0•4•Updated Oct 21, 2024Oct 21, 2024

    • reservoir

      Public
      Package registry for Lean/Lake.
      Vue
      •
      Apache License 2.0
      •1•17•6•1•Updated Oct 19, 2024Oct 19, 2024

    • lean4export

      Public
      Plain-text declaration export for Lean 4
      Lean
      •
      Apache License 2.0
      •6•12•3•1•Updated Oct 18, 2024Oct 18, 2024

    • vstte2024

      Public
      Lean
      •0•5•0•1•Updated Oct 15, 2024Oct 15, 2024

    • theorem_proving_in_lean4

      Public
      Theorem Proving in Lean 4
      leanlean4
      JavaScript
      •
      Apache License 2.0
      •96•167•30•18•Updated Oct 14, 2024Oct 14, 2024

    • SHerLOC

      Public
      A StableHLO analyzer in Lean
      Lean
      •
      Apache License 2.0
      •2•15•1•0•Updated Oct 9, 2024Oct 9, 2024

    • leansat

      Public archive
      This package provides an interface and foundation for verified SAT reasoning
      Lean
      •
      Apache License 2.0
      •6•51•5•1•Updated Aug 29, 2024Aug 29, 2024

    • vscode-lean

      Public
      Extension for VS Code that provides support for the older Lean 3 language. Succeeded by vscode-lean4 ('lean4' in the extensions menu) for the Lean 4 language.
      TypeScript
      •
      Apache License 2.0
      •49•116•53•20•Updated Aug 28, 2024Aug 28, 2024

    • SampCert

      Public
      SampCert : Verified Differential Privacy
      Lean
      •
      Apache License 2.0
      •7•66•4•5•Updated Aug 20, 2024Aug 20, 2024

    • LeanInk

      Public archive
      LeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4.
      visualizationleaninteractive-theorem-provinglean4alectryon
      Lean
      •
      Apache License 2.0
      •16•60•12•1•Updated Jul 18, 2024Jul 18, 2024

    • release-index

      Public
      Index of Lean releases
      0•0•0•0•Updated Jun 21, 2024Jun 21, 2024