Certified Research Reduction Graphs

Certified Research Reduction Graphs (CRRG) is a Lean based mathematical verification method to maintain the mathematical relationship between an open (unproven) statement and a proposed decomposition.

CRRG therefore should not be confused with a harness or an orchestration system. It does not decide what agents do, it decides whether the derives progress can enter the certified research state.

Problem Statement

Automated Research through AI agents is becoming the standard way to solve open problems in mathematics, cryptography, coding theory, and other similar fields. Examples include the Proximity Prize challenge, Prover Agent; and the AI Co-Mathematician.

Formal proofs provide a strong final reward gate for automated research, but in the above mentioned fields they are sparse. While a sparse reward gate is architecturally correct, it is difficult for agents to evaluate what partial progress looks like. There are examples attempting to assist autoresearch, no existing system (per my current knowledge) attempts to provide formally verified research state transitions within mathematical research.

Agents during research will attempt to prove part of the open problem or replace a harder obligation with an easier one. CRRG’s goal is to prove these transitions with a formal invariant to ensure the agents work contribute towards the global open problem.

Observation

During Lean 4 autoresearch I have been observing three distinct cases for attempts to use a blueprint to finalize a full formal proof of obligation.

1. **Conditional Lean Statements:**Attempting to use a conditional proof and close the conditional part. The main issue stems from the fact that conditional tells nothing about whether the missing statement is true, Lean accepts it as true and the Kernel compiles. Its useful for well accepted conjectures in human research, fragile in an autoresearch system.
2. Loss of target: Agent during progress silently drops a critical component without refutation, reformulates the problem and targets a statement that can never be closed. Reasons behind are context growth as research grows, unlucky compaction, but from the goal of using autoresearch to accelerate our understanding of mathematics what matters is the occurrence
3. Prestatements: Latest models use prestatements before solving, the problem is structural here. A) Prestatements before knowing the solution are incredible difficult B) Latest models still miss the correct frame, leave a mistake within. This component could be optimized further but CRRG is arguably the better solution.

These three observations lead to two distinct failure modes:

Infinite slicing -> Agents constantly avoid the hard open problem in favor of preparation. This leads to overreduction where the statement reaches a state thats unprovable and plausible unrefutable

Circling -> Agents reformulate the obligation to close the open problem to the same statement under different name. Over 100s of iterations of autonomous runs they use the same attempt on the same problem, believing they are narrowing down the statement and families of solutions.

The practical solution, currently, is researchers directing and steering the agents manually. Since March of this year I have seen countless discussions about this exact situation and it does produce results.

I believe the mistake in this approach is resource allocation. Top level researchers are better positioned to think about the problem and solution, rather than coaching.

CRRG should therefore be a bridge that closes this gap and enable human researchers to focus on what I refer to as theoretical mathematics.

Foundations

Formal verification is increasingly used in cryptographic research. For Lean-native mathematical and software-development tasks, kernel-checked proofs provide the optimal methodology for admitting agent-generated results [Lean Language Reference]. An autonomous research system for cryptography should therefore combine:

• Modular formal-verification system, using Interactive Oracle Reductions (IORs), a dynamically composed IOR statement to validate end-to-end soundness, and a verified Lean–Rust interface to ensure faithful implementation.
• Multi-agent autoresearch, providing a naturally strong setup to attack the problem component by component.
• Certified research state within the autoresearch loop. Human researchers approach a global problem, prove partial results, backtrack at refuted routes, until finally they start seeing the full solution. Agents need a system where they are also able to hold the full research state and hold the final target against adversarial conditions.

Agents could maintain a full research tree with conditional subtargets they are attempting to prove, navigate between the different leaves, and find the optimal path to an unconditional proof using the system. The transitions would carry a witness that only enables faithful modifications to the certified research state.

The first component (formal verification) is not complete, but it is the subject of significant ongoing effort. What remains missing is certified research state, to ensure mathematically valid reductions of the open problem can enter the research state. Investigating whether these components can share a common formal architecture is motivated by:

1. Unifying them reuses the efforts within formal verification, instead of introducing a distinct methodology.
2. Reusing formal verification methods composes better within an automated research system. Additionally it easily composes at discharge of the proof to the previously references formal verification.

The idea traces its direct lineage through the ArkLib IOR component called guarded CWSS to the CWSS framework outlined in Lattice-Based Polynomial Commitments: Towards Asymptotic and Concrete Efficiency [Fenzi, Moghaddas, and Nguyen]

The idea of the principle developed through the ArkLib IOR implementation, where the CWSS implementation provided the first anchor, and the guarded CWSS provided the strongest anchor to what the desired CRRG implementation should serve.

Guarded CWSS was the proof of concept that formal composition boundaries deserve to be first-class mathematical objects.

CRRG generalizes this idea from compositional cryptographic protocols to compositional mathematical research.

CRRG decides whether the derivation contributes the proof of the larger open obligation without knowing the full solution.

Mechanism

The mechanism creates a secondary invariant to solve the issue of sparse reward signals for long horizon autoresearch. The proposed Certified Research Reduction Graph is a dynamic system in which state transitions preserve the existing global target statement, and the local transitions are certified transformations of the global obligations.

A key required property of the targeted mechanism is dynamic extensibility without additional trust surface. Trusting agents for the local invariants is the not desired alternative on one end of the spectrum, any invariant entering the system should aim for a trustless design. Agents propose refinements that CRRG certifies that the obligation doesn’t weaken the the global statement and has a strict mathematical relationship to it.

For concrete examples, reductions must preserve the parent obligation, a refutation should clearly establish what part of the graph is actually refuted. Agents can open multiple parallel leaves on the tree and they can traverse the research state.

Two main alternatives were explored and eliminated, conditional statements were found to be too lose in live research on the proximity gap problem, and prestatements were found to be too rigid and difficult for a complex open problem.

Certified Research Transitions

At step t, an agent proposes a typed transition aₜ against the current certified research state Sₜ. The proposal declares its transition type τₜ—such as closure, refinement, exhaustive split, or refutation—and includes a machine-checkable witness wₜ.

The transition-specific verifier V_τₜ checks that the proposed mutation is valid and preserves the relevant obligation. The certified research state changes only after successful verification:

$$V_{\tau_t}(S_t,a_t,w_t)=1\quad\Longrightarrow\quad S_{t+1}=\operatorname{Apply}_{\tau_t}(S_t,a_t)$$

If verification fails, the certified state remains unchanged:

$$V_{\tau_t}(S_t,a_t,w_t)=0\quad\Longrightarrow\quad S_{t+1}=S_t$$

Accepted transition:

$$S_t\xrightarrow{\tau_t,a_t,w_t}S_{t+1}$$

Where:

• Sₜ is the faithful certified research state.
• τₜ identifies the transition type.
• aₜ specifies the proposed state mutation.
• wₜ is its machine-checkable witness.
• V_τₜ is the verifier for transition type τₜ.
• Apply_τₜ commits an accepted mutation.

Rejected transition:

An agent proposes to refine P into B alone:

$$P\xrightarrow{\mathrm{refine},w}B$$

The witness w cannot establish B ⊢ P without an unstated assumption A. What the agent actually holds is:

$$A\land B\vdash P$$

The verifier rejects because the proposed transition claims B ⊢ P, but w only proves the conditional A ∧ B ⊢ P. The assumption A is not an open obligation in the graph as it was silently dropped.

$$V_{\mathrm{refine}}(S_t,a,w)=0\quad\Longrightarrow\quad S_{t+1}=S_t$$

Correct transition — explicit split:

$$P\xrightarrow{\mathrm{split},w}\{A,B\}\qquad\text{where }w\text{ proves }A\land B\vdash P$$

Both A and B enter the graph as open obligations. Nothing is hidden.

$$V_{\mathrm{split}}(S_t,a,w)=1\quad\Longrightarrow\quad S_{t+1}=\operatorname{Apply}_{\mathrm{split}}(S_t,a)$$

Note: even a valid split increases the number of open obligations. Whether this is strategically beneficial depends on the research stage.

Agent exploration may remain in a separate working state, but it cannot modify the certified state without an accepted transition witness:

Propose → verify → commit or reject.

This produces proof-carrying research transitions and makes transitions themselves first-class mathematical objects.

CRRG does not determine strategic usefulness. A valid transition that’s strategically not useful would be for example:

$$P\xrightarrow{\mathrm{refine},w_1}\mathrm{Weil}_{eq}\xrightarrow{\mathrm{refine},w_2}Q_{\mathrm{unknown}}$$

Both transitions pass:

$$V_{\mathrm{refine}}(S_0,a_1,w_1)=1\quad\Longrightarrow\quad\mathrm{Weil}_{eq}\vdash P$$ $$V_{\mathrm{refine}}(S_1,a_2,w_2)=1\quad\Longrightarrow\quad Q_{\mathrm{unknown}}\vdash\mathrm{Weil}_{eq}$$

Both are sound. The decomposition holds: Q_unknown ⊢ P. CRRG certifies the chain.

But the second reduction is strategically destructive since Weil is established mathematics while the new mutation shifts it to an unknown open problem.

Prototype Status

A prototype for CRRG has been implemented in Lean and has been actively used on a live Reed-Solomon autoresearch deployment. The deployment has already produced:

• Certified refinements and closures
• Caught live semantic drift
• Deduplicated identical obligations
• Mechanically distinguished stalled research from certified state progress.

The prototype validated the mechanism’s operation, it does not establish improved formal discovery efficiency.

These should be established in a formal closed experiment.

The prototype does not currently have formally closed transitions, establishing those in Lean is part of the planned research.

CRRG Repository

Claim

CRRG enables untrusted agents to dynamically decompose mathematical statements in an automated research program. It prevents unsound weakening of target statements from entering the research state and through its verifiers closure of the CRRG tree implies the closure of the root statement.

Whether this architecture improves the scalability and effectiveness of long horizon autoresearch is an empirical question to be evaluated. The currently released methodology writeups behind breakthroughs in open problems, in my opinion, supports that such system is beneficial for long horizon autonomous agent work by removing the constant coaching and steering for obvious dead ends by the human operator(s).

Research Question

Can CRRG dynamically be extended at the research frontier when the relationship between the compositional work to proving the open problem is not known beforehand?

Use-cases

1. Compute scaling -> Increase the number of agents working on the problem while reducing duplicate work through the graph structure

2. Participation scaling -> Decomposing larger challenges for large open problems and enabling collaborative open research via either

3. Multiple smaller subcompetitions

4. Collaborative bounties under one competition

5. Human research -> While the idea was driven by issues observed in agentic systems, human researchers also benefit from the system