Research Lorenz

Report

Lorenz Verifier Discipline

A paused Lean RLM harness whose export is proof-integrity discipline — scheduler, planner, and population store that only admits verifier-surviving artifacts — not claimed theorems.

Verdict Inconclusive

Published
May 2026
Verdict
Inconclusive
Verification
Provisional
Question
What proof-search discipline survived after the Lean RLM harness paused?
Intent
Preserve verifier-first patterns without claiming theorems or autonomous proof discovery.
Method
Audit scheduler, planner, population-store, and compiler-feedback gates as a protocol surface.
Next test
Run a small Lean benchmark through Open Problems Lab with the same admission rules.

Lorenz Verifier Discipline

Question

What proof-search discipline survived after the Lean RLM harness paused?

Context

Lorenz is a verifier-first research-language-model harness for Lean-grounded mathematics and a Club B ancestor of Open Problems Lab. The live policy is deliberately humble: bounded proof sketches, compiler-grounded edits, and a population store that admits artifacts only after integrity checks. The project is paused; its discipline — not its unfinished scaffolds — is what the Recursive Self Improvement Lab keeps.

flowchart LR
  sketch["Bounded proof sketch"]
  compiler["Lean compiler feedback"]
  store["Population store"]
  admit["Admit only survivors"]

  sketch --> compiler --> store
  compiler -->|"reject"| sketch
  store --> admit

Findings

  • Every edit is grounded in Lean compiler feedback; sketches and evolutionary proposals cannot bypass integrity checks to count as progress.
  • v0 is a scheduler, planner, and autopilot runner over a directed research graph with a local control plane.
  • The export of the program is proof-integrity, race, and lineage pattern — not claimed theorems.
  • Open Problems Lab reuses that discipline for a narrower, source-grounded target set with immutable hashes and adversarial fixtures.
  • In the RSI Lab map, Lorenz supplies the verify precedent: proposers may search, but admission owns truth.

Method

Many bounded proof-sketch attempts feed a population database; RLM and evolutionary components sit architecturally behind verifier admission. Architecture notes publish; unfinished Lean scaffolds stay private and are not treated as proved results.

Limits

  • No theorems are claimed.
  • The paused harness is evidence of proof-integrity patterning, not search performance or recursive self-improvement.
  • Unfinished Lean scaffolds remain private and unpromoted.
  • Discipline transfer to Open Problems Lab is methodological reuse, not a completed benchmark.

Artifact

No public notebook is attached. The lorenz worktree remains private; this report is the sealed status of the verifier discipline.

  • lean
  • rlm
  • proof-search
  • verification