Rainbow documentation
Rainbow is an open-source theorem prover written in Clojure. A small kernel checks every proof, and proofs are ordinary Clojure data. These pages document the open core, version 1.4.1. The code is on GitHub under Apache-2.0.
Every proof and lemma in the open core
- theorems
- 4,025
- definitions
- 1,205
- modules
- 1,184
- The Applied Higher-Order Functions catalogue 322
- Non-negative rationals 140
- Signed rationals 136
- Finite types, distributions and Markov chains 122
- Lemmas behind operations-research checks 104
- Matrices 100
- Algorithm guarantees 85
- Vectors 44
- Finite sums 37
- Natural numbers 29
- Sets 16
- Logic 15
- Graph algorithms 8
- Foundations 8
- Analysis 6
- Finite sets 5
- Rationals 4
- Binary numerals 2
- Data types 1
Getting started
What Rainbow is · Install · Check your first proof · Commands
Concepts
The calculus · Content addressing · Proof modules · Proof bundles · The trusted base · What "proved" means · Maturity levels
Proof language
Declarations and modules · Terms and binders · Universes · Inductive types · The elaborator · The REPL and tactics · Why it works this way
Guides
Verify a module · Prove a lemma about rationals · Prove a lemma about vectors · Reproduce a result · Share and check a bundle
Compared with others
Rainbow next to Lean, Agda and Coq
Changelog
What changed in each release, up to 1.4.1.