leanprover/lean4-samples leanprover/lean4-samples

  • Stars
    star
    49
  • Rank 585,874 (Top 12 %)
  • Language Lean
  • License
    Apache License 2.0
  • Created almost 3 years ago
  • Updated over 1 year ago
Twitter logo Share LinkedIn logo Share Facebook logo Share
leanprover/lean4-samples
github

leanprover

Reviews

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

Repository Details

Code samples for Lean 4

More Repositories

1

lean4

Lean 4 programming language and theorem prover
Lean
4,612
star
2

lean3

Lean Theorem Prover
C++
2,143
star
3

elan

The Lean version manager
Rust
282
star
4

vscode-lean4

Visual Studio Code extension for the Lean 4 proof assistant
TypeScript
157
star
5

theorem_proving_in_lean4

Theorem Proving in Lean 4
JavaScript
157
star
6

lean2

Lean theorem prover version 0.2 (it supports standard and HoTT modes)
C++
121
star
7

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.
TypeScript
117
star
8

lake

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

verso

Lean documentation authoring tool
Lean
96
star
10

logic_and_proof_lean3

CMU Undergrad Course
TeX
96
star
11

lean3-mode

Emacs mode for Lean
Emacs Lisp
69
star
12

fp-lean

Functional Programming in Lean
JavaScript
68
star
13

lean4-cli

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

doc-gen4

Document Generator for Lean 4
Lean
62
star
15

LeanInk

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

SampCert

SampCert : Verified Differential Privacy
Lean
59
star
17

tc

Reference type checker for the Lean theorem prover
Haskell
57
star
18

LNSym

Armv8 Native Code Symbolic Simulator in Lean
Lean
52
star
19

leansat

This package provides an interface and foundation for verified SAT reasoning
Lean
48
star
20

theorem_proving_in_lean

Theorem proving in Lean
Python
47
star
21

tutorial

Lean Tutorials
TeX
43
star
22

functional_programming_in_lean

A book about functional programming in Lean
38
star
23

lean-client-js

TypeScript
34
star
24

lean4-nightly

Nightly builds
22
star
25

lean.vim

Vim Script
18
star
26

lean4checker

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

reservoir

Package registry for Lean/Lake.
Vue
16
star
28

super

Superposition prover
Lean
15
star
29

presentations

lean-related presentations
TeX
15
star
30

SHerLOC

A StableHLO analyzer in Lean
Lean
15
star
31

leanprover.github.io

www
HTML
15
star
32

lean-action

GitHub action for standard CI in Lean projects
Shell
14
star
33

leanbv

Lean
11
star
34

lean4export

Plain-text declaration export for Lean 4
Lean
11
star
35

lean3-web-editor

Lean web editor
TypeScript
9
star
36

smt2_interface

Interface to SMT2 solvers
Lean
9
star
37

lean-llvm

Custom-built LLVM toolchain for use in Lean 4
5
star
38

cmu-15815-s15

CMU 15-815 Spring 2015 : Interactive Theorem Proving
JavaScript
4
star
39

subverso

Lean
3
star
40

mini_crush

Mini crush tactic example
Lean
3
star
41

deprecated-homebrew-lean

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

NKL

A formalization of the NKI ISA
Lean
2
star
43

mkleanbook

JavaScript
2
star
44

Lean.tmbundle

A TextMate bundle for the Lean language
2
star
45

lean4-pr-releases

Automated releases from leanprover/lean4 PRs
2
star
46

lean-nightly

Lean nightly builds
2
star
47

macports

macports repository for Lean
Shell
1
star
48

ppa-updater

Ubuntu PPA updater for Lean
Shell
1
star
49

emacs-dependencies

Auxiliary repository to store emacs packages required by Lean Emacs mode
Emacs Lisp
1
star
50

reservoir-index

Registry index for Reservoir
Lean
1
star
51

TensorLib

A verified tensor library in Lean
Lean
1
star
52

TenCert

Verified tensor compilation in Lean
Lean
1
star