Rainbow next to Lean, Agda and Rocq

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.5.5 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 (Lean’s kernel likewise accelerates Nat literals, with GMP). Reduction runs on a budget, and running out is reported as a resource limit. Type checking first tries a lazy comparison (head reduction, congruence on equal heads, one definition unfolded at a time) and falls back to the full comparison; the public kernel/definitionally-equal? is unchanged (CHANGELOG).

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 Rocq use an inductive family. A Rainbow theorem may inhabit any sort; Lean’s theorem accepts only propositions.

Axioms

Lean has #print axioms, Rocq 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 such as :constructive, :classical and :mathlib-complete-logic name the combinations (profile.clj). An axiom counts as a principle only by its content id, never by its name or provenance.

Writing proofs

Write proof terms directly, as most of the corpus does, or tactic programs, which are Clojure vectors of steps (repl.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.

Lean also serves as a second checker. For 1.5.0, every theorem in every checkpoint of the tree the release is generated from, 2,107 distinct theorems, was exported with its exact type and accepted by Lean 4.30.0 and by Lean 4.35.0. #print axioms agrees with Rainbow’s axiom report on every one, and each of the 2,276 statements negated with their proofs kept was rejected. This checks the exported theorems; it is not a proof about Rainbow’s kernel (CHANGELOG).

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 kernel files whose total length (1,712 lines) is pinned by a release test, the Clojure reader and compiler, the JVM and its SHA-256, 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 Rainbow Pro’s domain, where programs currently reach Level 5 and Level 6 is the target.

When another prover fits better

• You need a large library: Mathlib (Lean) or Mathematical Components (Rocq).
• 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, Rocq), or hole-driven development (Agda).
• You want proofs written mainly as dependently pattern-matched programs, or cubical type theory: Agda.
• You want programs from the prover: Rocq extracts to OCaml, Haskell and Scheme; Lean and Agda compile.
• You want a long track record. Rainbow is young and its API will change.