What Rainbow is

Rainbow is a theorem prover written in Clojure. You write definitions, statements and proofs as Clojure data, a small dependent-type kernel checks them, and the result is stored as immutable EDN. A proof is a value: you can diff it, hash it, send it to someone and check it again, and once checked it is a building block for the next proof.

Why Rainbow

Proofs are Clojure data. Statements and proof terms are vectors and maps built with ordinary Clojure functions, and a proof module is a namespace.

You can read the kernel. It is 1,364 lines in four files, and CI fails if that number changes. Search, tactics, elaboration and checkpoint loading sit outside it and only propose terms, so a bug there gets a proof rejected and cannot get a false one accepted. See the trusted base and the calculus it checks.

Axioms are explicit. A classical principle enters only as a named axiom declaration. The kernel computes the axioms behind each theorem, and lein verify prints them next to the result.

You can re-check any result yourself. Each declaration is named by the SHA-256 hash of its content. lein verify sends a module back through the kernel, lein reproduce rebuilds a recorded result from source and compares ids, and a proof bundle lets anyone check your proofs with the kernel alone.

What is in the open core

The repository, github.com/Flexiana/rainbow, is Apache-2.0 licensed. Release v1.4.1, which these docs describe, contains the kernel (kernel.clj, term.clj, environment.clj and canonical.clj in src/rainbow/), the elaborator, tactics and a baseline proof search.

It also holds about 5,000 machine-checked declarations: natural numbers, rationals and signed rationals, finite sums, order, convexity and duality, finite matrices, Markov chains, and theorems about the decision step of each of the 222 algorithms in the Applied Higher-Order Functions operations-research catalogue. The milestone drivers that built them are in src/rainbow/milestones/, the checkpoints and reports in artifacts/. A Lean 4 bridge in src/rainbow/foreign/ and foreign/lean/ does export, import and a verified round trip.

The open core covers maturity levels 1 to 3: the kernel and the mathematics. Levels 4–6 are in Rainbow Pro.

Where to go next

Install the repository, check your first proof and keep Commands at hand. To write proofs, start with declarations and the guide Prove a rational lemma. If you know another prover, read Rainbow next to Lean, Agda and Coq. What “proved” means tells you how much a checked theorem says. The reference has a page for each proof module with its statements, scope and axioms, and the changelog is the repository’s own.

Reporting a problem

Open an issue on GitHub. The most useful report is a theorem that says less than its name or docstring suggests: a premise it does not need, a trivially true statement, a quantifier over the wrong thing. Give the declaration name and what you expected it to say. Report a kernel bug privately first, through flexiana.com/contact.

Pull requests are welcome. CONTRIBUTING.md and Writing a new module say what a new theorem needs.