Rainbow next to Lean, Agda and Coq

Draft, under review by Rainbow’s authors.

Rainbow is a theorem prover written in Clojure. Proofs are immutable EDN values named by a hash of their content. The open core at v1.4.1 has the kernel, the elaborator and tactics, a baseline proof search, and about 5,000 checked declarations, from arithmetic, rationals and finite matrices to Markov chains and the decision steps of 222 operations-research algorithms.

The calculus

A term is a Clojure vector in one of these forms (term.clj):

[:sort level]            a universe
[:bound i]               a variable, as a de Bruijn index
[:const id levels]       a constant, by content id, with universe arguments
[:app f a]               application
[:lam type body mode]    lambda; mode is :explicit or :implicit
[:pi type body mode]     dependent function type
[:let type value body]   local definition
[:nat n]                 a natural-number literal

A constant points to its declaration by content id, such as "sha256:3506...". Names like equality/Eq are aliases, and equal content gets the same id under any name.

A Pi type lives at imax of its domain and body levels (kernel.clj), so Prop is impredicative, as in Lean. Definitional equality compares normal forms (kernel.clj) under beta, unfolding of :reducible and :semireducible definitions, let, recursors on constructors, eta for lambdas, and six natural-number operations computed natively on literals, each pinned to the content id of its definition. Reduction runs on a budget, and running out is reported as a resource limit.

An inductive block declares one type with parameters, its constructors and a recursor <alias>.rec (kernel.clj). Blocks have no indices, and a recursive occurrence must be a whole constructor field. Equality is Leibniz equality, a definition (equality.clj), where Lean and Coq use an inductive family. A Rainbow theorem may inhabit any sort; Lean’s theorem accepts only propositions.

Axioms

Lean has #print axioms, Coq Print Assumptions, and Agda’s --safe rejects postulates. Rainbow’s kernel records the axioms each accepted declaration depends on transitively (kernel.clj), and lein verify prints them per theorem. Excluded middle, propositional extensionality, proof irrelevance, function extensionality and choice are ordinary axiom declarations you add on purpose. Profiles from :constructive to :mathlib-complete-logic name the combinations (profile.clj).

Writing proofs

Write proof terms directly, as most of the corpus does, or tactic programs, which are Clojure vectors of steps (first_tactic_program.clj). Tactics, the elaborator and proof search sit outside the trusted base: the kernel checks whatever term they build. The elaborator translates explicit surface forms ([:forall ...], [:fn ...], [:app ...], [:-> ...]) and does not infer implicit arguments or unify. apply handles non-dependent function types only, and refine takes an explicit partial term with numbered holes.

The Lean 4 bridge

The bridge is pinned to Lean 4.30.0 (lean.clj, foreign/lean/README.md). RainbowExport.lean writes Lean’s ConstantInfo and Expr values as EDN. Rainbow translates the core expression forms with explicit and implicit binders, maps Lean’s Nat to its own, rejects unsafe declarations and anything else, and kernel-checks the result.

rainbow.foreign.lean-export goes the other way. The repository round-trips logic/function-composition and requires its universe parameters, type and body to come back unchanged; it is sort-polymorphic, so it goes to Lean as a def.

For Mathlib v4.30.0, a catalog read from its .olean files, with every proof :redacted, and an exporter of chosen statements feed an explicit concept map (Lean’s Eq to equality/Eq). The kernel confirms each translated statement is a type, the proofs are made natively in Rainbow, and lein verify prints each re-proof’s axiom profile.

When Rainbow fits

• You work on the JVM and want proofs as values to store, diff, hash, ship and re-check.
• You must state what a result trusts: four fixed-length kernel files, the Clojure compiler and the JVM, and an axiom set per theorem.
• You re-check proofs from others, or from untrusted automation, with the kernel alone (lein verify --bundle).
• Your statements are about finite, computable objects.
• You write automation in Clojure and let the kernel check its output.
• You want a maturity level on every result. Levels 1–3 are in the open core; Levels 4–6 are in Rainbow Pro.

When another prover fits better

• You need a large library: Mathlib (Lean) or Mathematical Components (Coq).
• You need indexed inductive families, mutual or coinductive types, quotients, or definitional proof irrelevance.
• You want an elaborator with implicit arguments, unification and a rich interactive tactic language (Lean, Coq), or hole-driven development (Agda).
• You want dependent pattern matching or cubical type theory: Agda.
• You want programs from the prover: Coq extracts to OCaml, Haskell and Scheme; Lean and Agda compile.
• You want a long track record. Rainbow is young and its API will change.