Lorenz

Can a research-language-model harness for Lean mathematics keep learning strictly downstream of the verifier, so that no sketch, policy, or evolutionary proposal can bypass compiler integrity to count as progress? The harness runs many bounded proof-sketch attempts, grounds every edit in Lean compiler feedback, and admits artifacts into the population store only after integrity checks. The live policy is deliberately humble: a small verifier-grounded tabular sampler; RLM and evolutionary components sit architecturally behind the population database.

v0 is a scheduler, planner, and autopilot runner over a directed research graph with a local control plane. Proof-integrity, race, and lineage patterns — not claimed theorems — are what the program exports. The project is paused; Open Problems Lab reuses that discipline for a narrower, source-grounded target set. Architecture notes publish here; the lorenz worktree and any unfinished Lean scaffolds remain private and are not treated as proved results.