Explore @leanprover Open Source projects

Lean (@leanprover)

leanprover

Stars
8,503
Global Org. Rank 2,809 (Top 0.9 %)
Registered over 10 years ago
Most used languages

Lean 46.8 %

TypeScript
8.5 %

JavaScript
8.5 %

TeX
6.4 %

Shell
6.4 %

C++
4.3 %

Emacs Lisp
4.3 %

Python
2.1 %

Vim Script
2.1 %

Haskell
2.1 %

HTML
2.1 %

Ruby
2.1 %

Rust
2.1 %

Vue 2.1 %

lean4

Lean 4 programming language and theorem prover

lean3

Lean Theorem Prover

elan

The Lean version manager

vscode-lean4

Visual Studio Code extension for the Lean 4 proof assistant

theorem_proving_in_lean4

Theorem Proving in Lean 4

lean2

Lean theorem prover version 0.2 (it supports standard and HoTT modes)

vscode-lean

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.

lake

**(Deprecated: Merged into Lean 4)** Lean 4 build system and package manager with configuration files written in Lean.

verso

Lean documentation authoring tool

logic_and_proof_lean3

CMU Undergrad Course

lean3-mode

Emacs mode for Lean

fp-lean

Functional Programming in Lean

lean4-cli

A Lean 4 library for configuring Command Line Interfaces and parsing command line arguments.

doc-gen4

Document Generator for Lean 4

LeanInk

LeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4.

SampCert

SampCert : Verified Differential Privacy

tc

Reference type checker for the Lean theorem prover

LNSym

Armv8 Native Code Symbolic Simulator in Lean

lean4-samples

Code samples for Lean 4

leansat

This package provides an interface and foundation for verified SAT reasoning

theorem_proving_in_lean

Theorem proving in Lean

tutorial

functional_programming_in_lean

A book about functional programming in Lean

lean-client-js

lean4-nightly

lean.vim

lean4checker

Replay the `Environment` for a given Lean module, ensuring that all declarations are accepted by the kernel.

reservoir

Package registry for Lean/Lake.

super

Superposition prover

presentations

lean-related presentations

SHerLOC

A StableHLO analyzer in Lean

leanprover.github.io

lean-action

GitHub action for standard CI in Lean projects

leanbv

lean4export

Plain-text declaration export for Lean 4

lean3-web-editor

Lean web editor

smt2_interface

Interface to SMT2 solvers

lean-llvm

Custom-built LLVM toolchain for use in Lean 4

cmu-15815-s15

CMU 15-815 Spring 2015 : Interactive Theorem Proving

subverso

mini_crush

Mini crush tactic example

deprecated-homebrew-lean

See https://github.com/Homebrew/homebrew-core/blob/master/Formula/lean.rb

NKL

A formalization of the NKI ISA

mkleanbook

Lean.tmbundle

A TextMate bundle for the Lean language

lean4-pr-releases

Automated releases from leanprover/lean4 PRs

lean-nightly

Lean nightly builds

macports

macports repository for Lean

ppa-updater

Ubuntu PPA updater for Lean

emacs-dependencies

Auxiliary repository to store emacs packages required by Lean Emacs mode

reservoir-index

Registry index for Reservoir

TensorLib

A verified tensor library in Lean

TenCert

Verified tensor compilation in Lean