CRRG

The question

An agent can spend days preparing to solve a theorem, repeatedly restating the problem or silently losing a premise. How do we preserve a faithful account of the research between the start and the final proof?

Certified Research Reduction Graphs grew out of those failures in Lean-based autoresearch. A final proof gate is essential, but it says little about the intermediate state of a long investigation.

The mechanism

Agents can speculate freely. A change to the certified research state needs a machine-checkable witness:

Propose → verify → commit or reject.

A refinement must preserve its relationship to the original obligation. An exhaustive split must account for all its branches. A refutation must disprove the exact statement. A failed check leaves the certified state unchanged.

The core frontier invariant expresses that closing the current obligations closes the original root:

$$\left(\forall t,\; \operatorname{claim}(\operatorname{leaf}(t))\right) \;\Longrightarrow\; \operatorname{claim}(\operatorname{root}).$$

What I built

The public project includes a Lean library for certified transitions and tooling for persistent obligations, semantic seals, research episodes, and evidence records. My work combines the research formulation with building and testing the prototype in an agent-driven research environment.

The public repository reports live use on Reed–Solomon research: certified refinements and closures, detection of semantic drift, and deduplication of repeated obligations.

What the evidence does—and does not—show

Those observations demonstrate the operation of the mechanism. They do not establish better theorem-discovery efficiency. A valid transition can still be a strategically poor move, and a larger graph is not inherently progress.

Novelty recognition, choosing the right theorem, and inventing the missing mathematical idea remain research problems. CRRG is a prototype addressing admissibility, persistence, and auditability of the research state.

The original essay records the September proposal; the repository contains the subsequent implementation and its current limitations.

Read the original research note →