leanprover/lean4

Stars
4,612
Rank 9,203 (Top 0.2 %)
Language Lean
License
Apache License 2.0
Created over 6 years ago
Updated 24 days ago

leanprover/lean4

leanprover

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Lean 4 programming language and theorem prover

This is the repository for Lean 4, which is being actively developed and published as nightly releases. Stable point releases are planned for a later date after establishing a robust release process.

About

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.

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