leanprover/lean3

This repository has been archived on 15/Oct/2023
Stars
2,143
Rank 21,528 (Top 0.5 %)
Language
C++
License
Apache License 2.0
Created over 11 years ago
Updated about 1 year ago

leanprover/lean3

leanprover

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

Lean Theorem Prover

Important Lean 3.4.2 is the latest release. It is also the last release for the Lean 3.x code base. We are currently developing Lean 4. For reporting bugs and bug fixes in Lean 3.x, please go to the community branch.

About

Installation

Stable and nightly binary releases of Lean are available on the homepage. For building Lean from source, see the build instructions.

lean4

Lean 4 programming language and 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