Lean Kernel Arena / con-ron

con-ron is con-leche ported to Rust: the same checking algorithm, but with its own term representation — expressions are hash-consed into per-constructor arrays and named by 32-bit handles, with a persistent tier for the environment and a scratch tier per declaration.

The port is verified against con-leche in two steps. A Lean twin of con-leche's pure checker, written over the same data structures as the Rust, is proved to refine con-leche's; and Aeneas translates the Rust checker back into Lean, where it is proved to refine the twin: where the Rust function succeeds, it computes what the twin computes. So con-leche's consistency statement — if it accepts a set of declarations then they have a model in set theory, and in particular no theorem of False is accepted — carries over to what this binary accepts, modulo Aeneas as a Rust-to-Lean translator and the unverified driver (reading the file, scheduling threads).

That makes it less a high-assurance verification effort of its own than a second body for the same verified checker: a proof accepted by both is protected against a bug in Lean's compiler or runtime — the bignum library included — which the Rust build does not share, while still resting on a machine-checked consistency argument.

Like con-leche it runs in --verified mode here (the mode the theorem is about), with four worker threads for the check phase; it ingests raw lean4export NDJSON with no preprocessor and no subprocess, and an axiom it does not recognise makes it decline the stream rather than reject it. Exit codes are the arena's: 0 accept, 1 reject, 2 decline, 3 error. Running out of memory is none of them — a failed allocation aborts the process (SIGABRT) — so exhaustion can never be read as a rejection.

Single-threaded it retires a little under half of con-leche's instructions, and on Mathlib about two thirds of nanoda's. Written by AI under close human supervision from Joachim Breitner at the Lean FRO.