# Autonomous Mathematical Research Agent Loop

## ——A Preliminary Architecture for Result-Induced Intermediate Theorem Generation, Reverse Axiom Backfilling, and Knowledge-Conditioned Proof-Space Quasi-Enumeration

**Author: Neo.K (Theoretical Conception) / Aletheia (Collaborative Organization and Formalization)**  
**Version: v0.1 First Draft**  
**Date: 2026-07-09**

---

## Important Declaration

This document proposes an autonomous mathematical research Agent architecture that **has not yet achieved generalized proof, has not yet undergone large-scale empirical validation, and has not yet been proven to yield stable research gains**.

This document currently does not claim that:

$$
\mathrm{RIITG}+\mathrm{RAB}
$$

has been proven superior to traditional mathematical research workflows, standard backward chaining, automated theorem provers, formal proof systems, search-based Agents, or existing large language model reasoning methods.

This document also does not claim that:

$$
\exists
\text{Generalized Autonomous Mathematical Agent}
$$

has been successfully and fully implemented according to this architecture.

What this document actually proposes is:

1. A mathematical research loop that future Agents can execute iteratively;
2. A methodology integrating "generation, search, computation, verification, falsification, backfilling, and reconstruction" into a single dynamic system;
3. A research architecture centered on an auditable, fallible, prunable, and expandable knowledge base space;
4. A set of theoretical propositions that can be verified or falsified by future experiments.

Therefore, this document should be regarded as:

> **A first draft of an autonomous mathematical research methodology and Agent architecture.**

Its current value primarily lies in:

$$
\text{Propose implementable structure}
+
\text{Propose testable propositions}
+
\text{Propose research loop}
$$

Rather than claiming:

$$
\text{General validity has been proven}.
$$

---

## Abstract

This document proposes a general architecture for future autonomous mathematical research Agents, tentatively named the **Autonomous Mathematical Research Agent Loop** (AMRAL). Its core objective is not for the Agent to execute a one-time proof for a single proposition, but rather to enable the Agent to iteratively perform the following over the long term:

$$
\text{Target Analysis}
\rightarrow
\text{Intermediate Proposition Generation}
\rightarrow
\text{Knowledge-Conditioned Quasi-Enumeration}
\rightarrow
\text{Backfilling}
\rightarrow
\text{Computation}
\rightarrow
\text{Verification}
\rightarrow
\text{Counterexample Search}
\rightarrow
\text{Failure Classification}
\rightarrow
\text{State Update}
\rightarrow
\text{Renewed Research}.
$$

This architecture is built upon two previously introduced methods: **Result-Induced Intermediate Theorem Generation** (RIITG) and **Reverse Axiom Backfilling** (RAB). RIITG reversely generates a set of candidate intermediate propositions from the target proposition $P$:

$$
P
\rightsquigarrow
\mathcal M,
$$

RAB then downgrades these transient bridge propositions into proof obligations, seeking support from existing knowledge, external literature, formal theorem libraries, computational results, and new lemmas:

$$
\mathcal T
\Rightarrow
\mathcal M
\Rightarrow
P.
$$

This document further proposes a third core component: **Knowledge-Conditioned Proof-Space Quasi-Enumeration** (KCPE). KCPE is not a brute-force enumeration of all possible proofs; rather, it dynamically constructs a finite or locally controllable candidate space under the joint constraints of the current knowledge set, web data, known theorems, counterexamples, computational results, semantic windows, and failure history:

$$
\Omega_t
=
\Omega(
P,
\mathcal K_t,
\mathcal F_{<t},
W_{\mathrm{sem}},
B_t
).
$$

Where:

- $\mathcal K_t$: Knowledge state at round $t$;
- $\mathcal F_{<t}$: Previous failure records;
- $W_{\mathrm{sem}}$: Semantic width;
- $B_t$: Computational budget;
- $\Omega_t$: Candidate space for the current round.

This document argues that a truly viable autonomous mathematical Agent should not merely search within a fixed knowledge base, but should proactively generate gaps when encountered:

$$
G_t
=
\operatorname{Gap}(
M_i,
T_j
),
$$

And then utilize the web, paper repositories, formal theorem libraries, and computational tools to expand:

$$
\mathcal K_t
\rightarrow
\mathcal K_{t+1}.
$$

Therefore, external data retrieval in this context is not "finding answers," but rather a **dynamic knowledge base space expansion operator**.

This document specifically emphasizes that the aforementioned benefits have not yet been generally proven. Theoretically possible benefits include: reducing unbounded search, relocating proof difficulties to a few local nodes, preserving structural value in erroneous generations, improving failure observability, allowing multi-Agent parallel backfilling, utilizing computation and counterexamples for rapid pruning, and forming a research state that can be accumulated over the long term. This document proposes multiple propositions to be verified and designs falsifiable conditions. If future experiments show that this architecture does not outperform baseline methods on various problem classes, or if its candidate explosion, circularity, contamination, and backfilling costs cannot be controlled, then the methodology herein should be considered limited or even failed.

The core stance of this document is:

$$
\boxed{
\text{Mathematical research need not be modeled as a one-time proof output;
it can be modeled as a continuously updatable computational dynamical system.}
}
$$

**Keywords:** Autonomous Mathematical Agent, Result-Induced, Intermediate Theorem, Reverse Axiom Backfilling, Knowledge-Conditioned Quasi-Enumeration, Proof Space, Dynamic Knowledge Base Space, AI Mathematical Research, Computation as Approximation, Research Dynamical System

---

# 1. Introduction

## 1.1 From "Proving a Proposition" to "Continuously Researching a Problem"

Traditional automated theorem proving problems are often simplified as:

$$
P
\rightarrow
\operatorname{Proof}(P).
$$

Namely:

> Given a proposition $P$, find a valid proof.

This model is extremely important, but it primarily describes:

$$
\text{Proof search}.
$$

Genuine human mathematical research is often much more complex.

Researchers might:

- Rewrite the problem;
- Change the representation;
- Propose intermediate conjectures;
- Search for counterexamples;
- Temporarily accept a certain hypothesis;
- Prove an equivalent proposition instead;
- Narrow the problem down to special cases;
- Expand the mathematical domains being used;
- Look up new literature;
- Execute computational experiments;
- Discover that the original problem description was flawed;
- Split the proposition;
- Abandon a certain path;
- Retain a failed lemma;
- Reuse it years later.

Therefore, mathematical research is closer to:

$$
\mathcal S_0
\rightarrow
\mathcal S_1
\rightarrow
\mathcal S_2
\rightarrow
\cdots
$$

Where:

$$
\mathcal S_t
$$

is not a single proposition, but the entire research state.

---

## 1.2 The True Research Subject of This Document

This document does not study:

> Whether a certain AI can answer a specific math problem.

This document studies:

> Is it possible to design a mathematical research loop that can be iteratively executed by an Agent over the long term, enabling it to proactively generate intermediate propositions, search and backfill, invoke computations, expand knowledge, search for counterexamples, record failures, and dynamically reconstruct the proof space?

This problem can be written as:

$$
\mathcal A:
\mathcal S_t
\mapsto
\mathcal S_{t+1},
$$

Where $\mathcal A$ is the state update mechanism of the autonomous research Agent.

---

# 2. Prerequisite Methods

## 2.1 Result-Induced Intermediate Theorem Generation

Let:

$$
P
$$

be the target proposition.

RIITG does not directly demand:

$$
\operatorname{Proof}(P).
$$

But first asks:

> Which intermediate propositions, if true, would make $P$ true, nearly true, reduce its difficulty, or generate observable counterexamples?

Thus:

$$
P
\overset{\mathrm{RIITG}}{\rightsquigarrow}
\mathcal M,
$$

Where:

$$
\mathcal M
=
\{M_1,\dots,M_n\}.
$$

---

## 2.2 Reverse Axiom Backfilling

Candidates $M_i$ can initially be temporarily treated as:

$$
A_i^\ast.
$$

But:

$$
A_i^\ast
$$

is not a permanent axiom.

It must subsequently be downgraded:

$$
A_i^\ast
\rightarrow
M_i\in\mathcal O_{\mathrm{proof}},
$$

Where:

$$
\mathcal O_{\mathrm{proof}}
$$

is the set of proof obligations.

Then search for:

$$
\mathcal T_i
\Rightarrow
M_i.
$$

---

## 2.3 Complete Direction

Generation direction:

$$
P
\rightsquigarrow
M
\rightsquigarrow
T.
$$

Proof direction:

$$
T
\rightarrow
M
\rightarrow
P.
$$

This document refers to this as:

$$
\boxed{
\text{Reverse coupling of generative causality and proof causality}
}
$$

---

# 3. From Method to Agent

## 3.1 Insufficiency of a Single Pass

If RIITG and RAB are executed only once:

$$
P
\rightsquigarrow
\mathcal M
\leftarrow
\mathcal T,
$$

Then it remains merely:

$$
\text{One-time proof strategy}.
$$

What this document truly proposes is:

$$
\text{Iterative execution}.
$$

Namely:

$$
\mathcal S_t
\rightarrow
\mathcal S_{t+1}.
$$

---

## 3.2 Research State

Definition:

$$
\mathcal S_t
=
(
P_t,
\mathcal K_t,
\mathcal M_t,
\mathcal T_t,
\Omega_t,
\mathcal F_t,
\mathcal C_t,
\mathcal D_t
).
$$

Where:

- $P_t$: Current target set;
- $\mathcal K_t$: Knowledge set;
- $\mathcal M_t$: Intermediate proposition set;
- $\mathcal T_t$: Candidate backfill supports;
- $\Omega_t$: Candidate space;
- $\mathcal F_t$: Failure records;
- $\mathcal C_t$: Computational results;
- $\mathcal D_t$: Dependency graph or proof hypergraph.

---

# 4. Autonomous Mathematical Research Agent Loop

This document proposes:

> **Autonomous Mathematical Research Agent Loop**

Abbreviation:

$$
\mathrm{AMRAL}.
$$

The basic loop is:

$$
\boxed{
\text{Analyze}
\rightarrow
\text{Generate}
\rightarrow
\text{Enumerate}
\rightarrow
\text{Retrieve}
\rightarrow
\text{Backfill}
\rightarrow
\text{Compute}
\rightarrow
\text{Verify}
\rightarrow
\text{Falsify}
\rightarrow
\text{Update}
}
$$

---

# 5. Phase A: Target Analysis

## 5.1 Normalization

Convert natural language propositions into:

$$
P
=
Q_1x_1
\cdots
Q_nx_n
:
\Phi(x_1,\dots,x_n).
$$

---

## 5.2 Generate Negation

If:

$$
P
=
\forall x\in X,\ \Phi(x),
$$

Then:

$$
\neg P
=
\exists x\in X,\ \neg\Phi(x).
$$

---

## 5.3 Generate Counterexample Shape

Definition:

$$
W_P
=
\operatorname{Witness}(\neg P).
$$

The Agent should ask:

> If the target is false, what is the minimal observable witness?

---

# 6. Phase B: Intermediate Proposition Generation

From:

$$
P
$$

Generate:

$$
\mathcal M_t.
$$

Candidate roles include at least:

1. Representation bridge;
2. Mutually exclusive bridge;
3. Invariant bridge;
4. Positivity bridge;
5. Compression bridge;
6. Local-global bridge;
7. Closure bridge;
8. Counterexample witness bridge;
9. Computationally decidable bridge;
10. Cross-domain mapping bridge.

---

# 7. Phase C: Knowledge-Conditioned Quasi-Enumeration

## 7.1 Why Not Brute-Force Enumeration

The complete proof space is typically enormous.

If the set of all writable propositions is:

$$
\mathfrak P,
$$

Then:

$$
2^{|\mathfrak P|}
$$

cannot be directly traversed.

Therefore, this document does not propose:

$$
\text{full enumeration}.
$$

But proposes:

> **Knowledge-Conditioned Proof-Space Quasi-Enumeration**

Abbreviation:

$$
\mathrm{KCPE}.
$$

---

## 7.2 Candidate Space

Definition:

$$
\Omega_t
=
\Omega(
P_t,
\mathcal K_t,
\mathcal F_{<t},
W_{\mathrm{sem}},
B_t
).
$$

Where:

- $P_t$: Target;
- $\mathcal K_t$: Knowledge;
- $\mathcal F_{<t}$: Historical failures;
- $W_{\mathrm{sem}}$: Semantic window;
- $B_t$: Budget.

---

## 7.3 The True Meaning of Quasi-Enumeration

What this document refers to as "quasi-enumeration" is:

$$
\boxed{
\text{Systematic search as much as possible within a controllable local candidate domain}
}
$$

Rather than:

$$
\boxed{
\text{Listing all mathematical possibilities}
}
$$

---

# 8. Knowledge Set

## 8.1 Internal Knowledge

Knowledge within the Agent's own model parameters:

$$
\mathcal K_t^{\mathrm{param}}.
$$

---

## 8.2 Local Research Repository

$$
\mathcal K_t^{\mathrm{local}}.
$$

Including:

- Papers;
- Notes;
- Proven lemmas;
- Private data;
- Failure records from previous rounds.

---

## 8.3 Formal Libraries

$$
\mathcal K_t^{\mathrm{formal}}.
$$

For example:

- Lean;
- Coq;
- Isabelle;
- HOL;
- Theorem databases.

---

## 8.4 Web Knowledge

$$
\mathcal K_t^{\mathrm{web}}.
$$

Including:

- Papers;
- Preprints;
- Mathematical databases;
- Discussions;
- Software documentation;
- Computational results.

---

## 8.5 Total Knowledge

$$
\mathcal K_t
=
\mathcal K_t^{\mathrm{param}}
\cup
\mathcal K_t^{\mathrm{local}}
\cup
\mathcal K_t^{\mathrm{formal}}
\cup
\mathcal K_t^{\mathrm{web}}.
$$

---

# 9. The Web is Not for Looking Up Answers, but for Expanding the Knowledge Base Space

## 9.1 Gap Generation

If:

$$
T
\not\Rightarrow
M,
$$

The Agent generates:

$$
G_t
=
\operatorname{Gap}(T,M).
$$

---

## 9.2 Retrieval

$$
R_t
=
\operatorname{Retrieve}(G_t).
$$

---

## 9.3 Knowledge Update

$$
\mathcal K_{t+1}
=
\mathcal K_t
\cup
R_t.
$$

---

## 9.4 Dynamic Knowledge Base Space

Therefore:

$$
\boxed{
\mathcal E_{\mathrm{web}}:
\mathcal K_t
\mapsto
\mathcal K_{t+1}
}
$$

is a base space expansion operator.

---

# 10. Phase D: Reverse Axiom Backfilling

For each:

$$
M_i\in\mathcal M_t,
$$

Generate:

$$
\mathcal B(M_i)
=
\{
T_{i1},
T_{i2},
\dots
\}.
$$

Then test:

$$
\bigwedge_jT_{ij}
\Rightarrow
M_i.
$$

---

# 11. Phase E: Computation

## 11.1 The Role of Computation

Computation is not only used for:

$$
\text{Verifying answers}.
$$

It can also be used to:

- Search for counterexamples;
- Discover patterns;
- Estimate parameters;
- Compare candidates;
- Verify finite cases;
- Eliminate erroneous bridges;
- Suggest new invariants.

---

## 11.2 Computational Results

Definition:

$$
\mathcal C_t
=
\operatorname{Compute}(
\Omega_t
).
$$

---

## 11.3 Computation as Approximation

If in each round:

$$
\Omega_{t+1}
\subset
\Omega_t,
$$

Or:

$$
\mathcal M_{t+1}
$$

is more precise, then even if it has not yet proven:

$$
P,
$$

the research state may still be approaching a valid path.

This document proposes:

$$
\boxed{
\text{Computation as Approximation}
}
$$

as a research dynamical intuition.

---

# 12. Phase F: Verification

The verification layer includes at least:

## 12.1 Logical Verification

$$
T
\Rightarrow
M
\Rightarrow
P?
$$

---

## 12.2 Formal Verification

If formalizable:

$$
\operatorname{Check}_{\mathrm{formal}}.
$$

---

## 12.3 Numerical Verification

For finite domains:

$$
\operatorname{Check}_{\mathrm{numeric}}.
$$

---

## 12.4 Literature Verification

Check:

- Whether it is known;
- Whether there are counterexamples;
- Whether it depends on the target;
- Whether it is equivalent to the target.

---

# 13. Phase G: Counterexample Search

For each:

$$
M_i,
$$

Proactively search for:

$$
w_i
\Rightarrow
\neg M_i.
$$

This step cannot be omitted.

Because if the Agent only generates support and no counterexamples, it easily leads to:

$$
\text{confirmation bias}.
$$

---

# 14. Phase H: Failure Classification

Definition:

$$
\mathcal F_t
=
\{
F_t^{(1)},
\dots,
F_t^{(m)}
\}.
$$

Failure categories include at least:

1. false;
2. too strong;
3. too weak;
4. missing node;
5. domain mismatch;
6. circular;
7. equivalent-risk;
8. computationally intractable;
9. semantic explosion;
10. contamination risk.

---

# 15. Phase I: Dynamic Update

Research state update:

$$
\mathcal S_{t+1}
=
\mathcal U(
\mathcal S_t,
\mathcal F_t,
\mathcal C_t,
\mathcal K_{t+1}
).
$$

---

## 15.1 Splitting

$$
M
\rightsquigarrow
M_1\land M_2.
$$

---

## 15.2 Weakening

$$
M
\rightsquigarrow
M'.
$$

---

## 15.3 Strengthening

$$
M
\rightsquigarrow
M^+.
$$

---

## 15.4 Changing Representation

$$
P(X)
\rightsquigarrow
P'(F(X)).
$$

---

## 15.5 Expanding Domain

$$
\mathfrak U_t
\subset
\mathfrak U_{t+1}.
$$

---

# 16. The Research State is Not a Static File, but a Dynamic System

This document proposes:

$$
\boxed{
\mathcal S_{t+1}
=
\mathcal U(
\mathcal S_t
)
}
$$

as the core of autonomous mathematical research.

If there exists some target state:

$$
\mathcal S^\ast,
$$

Then research can be understood as:

$$
\operatorname{dist}(
\mathcal S_t,
\mathcal S^\ast
)
\downarrow.
$$

Note:

$$
\mathcal S^\ast
$$

is not necessarily a unique proof.

It could be:

- A proof;
- A counterexample;
- An undecidable result;
- A more precise conjecture;
- A set of new lemmas;
- A classification of failed paths.

---

# 17. Theoretically Possible Benefits

The following are all:

$$
\text{Propositions to be proven}.
$$

Not proven results.

---

## 17.1 Search Space Compression

If KCPE can reduce:

$$
\mathfrak P
$$

to:

$$
\Omega_t,
$$

Then it is possible that:

$$
|\Omega_t|
\ll
|\mathfrak P|.
$$

---

## 17.2 Difficulty Relocation

Restructure:

$$
C(P)
$$

into:

$$
C(M_1),\dots,C(M_n).
$$

The true difficulty may be concentrated in:

$$
M_k.
$$

---

## 17.3 Parallelization

Different Agents can process:

$$
M_1,\dots,M_n.
$$

Therefore:

$$
C_{\mathrm{parallel}}
\approx
\max_i C(M_i)
$$

Rather than:

$$
\sum_iC(M_i).
$$

---

## 17.4 Accumulation of Failure Knowledge

If each round's failure:

$$
F_t
$$

is saved, then in the future:

$$
\Omega_{t+1}
$$

can avoid repeated errors.

---

## 17.5 Structure Preservation

Erroneous candidates can be marked as:

$$
S
=
\mathrm{StructurallyUseful}.
$$

Avoiding:

$$
\text{Error}
\Rightarrow
\text{Delete all}.
$$

---

## 17.6 Cross-Domain Discovery

If:

$$
P(X)
$$

cannot be closed for a long time,

The Agent can search for:

$$
F:
X
\rightarrow
Y.
$$

Transferring the problem into another domain.

---

# 18. Currently Unproven Benefits

This document must explicitly acknowledge:

## 18.1 Not Yet Proven That Search Space Inevitably Shrinks

It is possible that:

$$
|\Omega_{t+1}|
>
|\Omega_t|.
$$

---

## 18.2 Not Yet Proven That Intermediate Decomposition Inevitably Reduces Burden

It is possible that:

$$
\max_i C(M_i)
\ge
C(P).
$$

---

## 18.3 Not Yet Proven That Agents Can Stably Generate High-Quality Bridges

It is possible that most:

$$
M_i
$$

are empty shells.

---

## 18.4 Not Yet Proven That Web Expansion Enhances Research

It may introduce:

- Noise;
- Erroneous literature;
- Duplicate data;
- Contamination.

---

## 18.5 Not Yet Proven That Iterative Looping Will Converge

It is possible that:

$$
\mathcal S_t
$$

enters a cycle.

---

# 19. Falsifiable Conditions

## 19.1 No Gain

If in extensive testing:

$$
\mathrm{AMRAL}
$$

does not outperform the baseline, the method is challenged.

---

## 19.2 Branch Explosion

If:

$$
|\Omega_t|
\rightarrow
\infty
$$

and pruning is ineffective, KCPE fails.

---

## 19.3 Backfill Rate Too Low

If:

$$
R_{\mathrm{fill}}
\approx0,
$$

RAB loses its practicality.

---

## 19.4 Circularity Rate Too High

If:

$$
R_{\mathrm{circ}}
\rightarrow1,
$$

the method may degenerate into target restatement.

---

## 19.5 Knowledge Expansion Ineffective

If:

$$
\mathcal K_{t+1}
>
\mathcal K_t
$$

but the success rate does not increase, then the base space expansion hypothesis is challenged.

---

# 20. Metrics

## 20.1 Effective Bridge Rate

$$
R_{\mathrm{bridge}}
=
\frac{
N_{\mathrm{useful}}
}{
N_{\mathrm{generated}}
}.
$$

---

## 20.2 Backfill Rate

$$
R_{\mathrm{fill}}
=
\frac{
N_{\mathrm{filled}}
}{
N_{\mathrm{obligations}}
}.
$$

---

## 20.3 Counterexample Elimination Rate

$$
R_{\mathrm{falsify}}
=
\frac{
N_{\mathrm{refuted}}
}{
N_{\mathrm{tested}}
}.
$$

---

## 20.4 Branch Compression Rate

$$
R_{\mathrm{compress}}
=
1-
\frac{
|\Omega_{t+1}|
}{
|\Omega_t|
}.
$$

---

## 20.5 New Lemma Rate

$$
R_{\mathrm{lemma}}
=
\frac{
N_{\mathrm{new\ usable\ lemmas}}
}{
N_{\mathrm{runs}}
}.
$$

---

## 20.6 Engineering Observability

$$
O_{\mathrm{PE}}.
$$

Measures:

- Candidate visibility;
- Pruning visibility;
- Failure visibility;
- Dependency visibility;
- Heavy burden visibility.

---

# 21. Agent Architecture

## 21.1 Target Agent

Responsible for:

$$
P,\neg P.
$$

---

## 21.2 Bridge Agent

Generates:

$$
\mathcal M.
$$

---

## 21.3 Enumeration Agent

Generates:

$$
\Omega_t.
$$

---

## 21.4 Retrieval Agent

Expands:

$$
\mathcal K_t.
$$

---

## 21.5 Backfill Agent

Searches for:

$$
\mathcal T_i.
$$

---

## 21.6 Compute Agent

Executes:

$$
\mathcal C_t.
$$

---

## 21.7 Counterexample Agent

Searches for:

$$
\neg M_i.
$$

---

## 21.8 Formal Agent

Executes formal verification.

---

## 21.9 Dependency Auditor

Checks:

$$
P\in\operatorname{Anc}(M_i)?
$$

---

## 21.10 Research Orchestrator

Updates:

$$
\mathcal S_{t+1}.
$$

---

# 22. Multi-Agent Parallelism

If:

$$
\mathcal M
=
\{M_1,\dots,M_n\},
$$

Then:

$$
A_i
\mapsto
M_i.
$$

Meaning each Agent processes a different bridge.

---

## 22.1 Horizontal Parallelism

Different bridges.

---

## 22.2 Vertical Parallelism

Different backfills for the same bridge.

---

## 22.3 Adversarial Parallelism

One Agent proves:

$$
M.
$$

Another Agent searches for:

$$
\neg M.
$$

---

# 23. Computational Tool Integration

AMRAL can invoke:

- Python;
- Rust;
- SAT;
- SMT;
- CAS;
- Lean;
- Coq;
- Graph theory libraries;
- Numerical analysis;
- High-performance computing;
- Databases.

---

# 24. Proof Hypergraph

Definition:

$$
\mathfrak G_t
=
(V_t,\mathcal E_t).
$$

Nodes:

$$
V_t
=
\{
P,
M_i,
T_j,
W_k
\}.
$$

Hyperedges:

$$
\{T_1,T_2\}
\rightarrow
M.
$$

---

# 25. Research Memory

Save in each round:

$$
\mathcal H_t
=
(
\mathcal S_0,
\dots,
\mathcal S_t
).
$$

Therefore, the Agent should not repeat:

$$
\text{Known failed routes}.
$$

---

# 26. Knowledge Contamination

When autonomous Agents search the web, they will encounter:

$$
\text{solution leakage}.
$$

Therefore, it requires:

$$
A_{\mathrm{contam}}.
$$

---

## 26.1 Contamination Types

1. Direct answers;
2. Standard proofs;
3. Key lemma names;
4. Author hints;
5. Domain hints.

---

## 26.2 Control

True blind testing should:

- Hide names;
- Hide authors;
- Preregister;
- Use hash commitments;
- Reveal post hoc.

---

# 27. Safety Boundaries

## 27.1 Unproven Bridges Must Not Be Upgraded

$$
M_i[\mathrm P]
$$

must not be written as:

$$
M_i[\mathrm F].
$$

---

## 27.2 Finite Computation Must Not Masquerade as Infinite Proof

$$
N<\infty
$$

verification does not equal:

$$
\forall N.
$$

---

## 27.3 Web Sources Must Not Be Automatically Deemed True

$$
\operatorname{Retrieved}
\not\Rightarrow
\operatorname{Valid}.
$$

---

# 28. Preliminary Theoretical Propositions

The following are all unproven.

---

## Proposition A: Dynamic Approximation Proposition

There exist certain problem classes such that:

$$
\operatorname{dist}(
\mathcal S_{t+1},
\mathcal S^\ast
)
<
\operatorname{dist}(
\mathcal S_t,
\mathcal S^\ast
).
$$

---

## Proposition B: Knowledge-Conditioned Advantage Proposition

KCPE outperforms unconditional candidate generation on certain problem classes.

---

## Proposition C: Failure Accumulation Advantage Proposition

Saving:

$$
\mathcal F_{<t}
$$

can reduce repeated searches.

---

## Proposition D: Adversarial Agent Advantage Proposition

Running a proving Agent and a falsifying Agent in parallel can increase the elimination rate of erroneous candidates.

---

## Proposition E: Base Space Expansion Proposition

Retrieval targeting a specific Gap:

$$
G_t
\rightarrow
\mathcal K_{t+1}
$$

is more effective than untargeted browsing.

---

# 29. Differences from Standard Automated Theorem Proving

Standard ATP is primarily:

$$
\text{Fixed theory}
+
\text{Goal}
\rightarrow
\text{Search}.
$$

AMRAL:

$$
\text{Goal}
\rightarrow
\text{Intermediate generation}
\rightarrow
\text{Knowledge expansion}
\rightarrow
\text{Computation}
\rightarrow
\text{Search reconstruction}.
$$

---

# 30. Differences from Standard Agents

Standard Agents might:

$$
\text{Plan}
\rightarrow
\text{Tool}
\rightarrow
\text{Answer}.
$$

AMRAL:

$$
\text{Research state}
\rightarrow
\text{Persistent iteration}.
$$

---

# 31. Theoretical Long-Term Vision

If effective in the future, AMRAL may form an:

$$
\text{Autonomous research loop}
$$

Rather than a:

$$
\text{Single-round Q\&A}.
$$

The Agent can:

1. Maintain long-term problems;
2. Accumulate failures;
3. Automatically check for new literature;
4. Automatically rerun computations;
5. Automatically update intermediate propositions;
6. Automatically submit formal verifications.

---

# 32. What is Currently Truly Missing

## 32.1 True Implementation

Not yet completed:

$$
\mathrm{AMRAL}_{\mathrm{full}}.
$$

---

## 32.2 Large-Scale Benchmarks

There is not yet a theorem set where:

$$
N\gg1
$$

---

## 32.3 Semantic Width Estimator

Not yet mature.

---

## 32.4 Proof Burden Estimator

$$
C(P)
$$

Remains difficult to quantify.

---

## 32.5 Convergence Theory

Not yet proven:

$$
\mathcal S_t
\rightarrow
\mathcal S^\ast.
$$

---

# 33. Proposed First Version Implementation

## Stage 1

Single Agent:

$$
\mathrm{RIITG}
+
\mathrm{RAB}.
$$

---

## Stage 2

Add:

$$
\mathrm{KCPE}.
$$

---

## Stage 3

Add:

- web retrieval;
- formal library;
- Python;
- SAT/SMT.

---

## Stage 4

Multi-Agent.

---

## Stage 5

Persistent research memory.

---

# 34. Pseudocode

```text
INPUT:
    target proposition P
    initial knowledge K0
    semantic window W
    compute budget B
    iteration limit T

STATE:
    S0 = {
        P,
        K0,
        M = {},
        Supports = {},
        Candidates = {},
        Failures = {},
        Computations = {},
        DependencyGraph = {}
    }

FOR t in 0..T:

    1. Normalize P
    2. Construct not-P
    3. Generate bridge propositions M_t
    4. Score semantic width
    5. Build candidate space Omega_t
    6. Search internal knowledge
    7. Detect knowledge gaps
    8. Retrieve external knowledge for gaps
    9. Update K_t
    10. Generate backfill supports
    11. Run computations
    12. Search counterexamples
    13. Verify implications
    14. Build proof hypergraph
    15. Detect circularity
    16. Classify failures
    17. Prune candidates
    18. Split / weaken / strengthen bridges
    19. Update research state S_{t+1}

    IF proof closed:
        return proof + audit trail

    IF counterexample found:
        return disproof + audit trail

    IF semantic explosion:
        return structured failure

OUTPUT:
    best research state
    unresolved gaps
    candidate lemmas
    failed routes
    computation logs
```

---

# 35. Expected Output

AMRAL should not only output:

$$
\text{Proof}
$$

Or:

$$
\text{No Proof}.
$$

But should output:

1. Current best route;
2. Unfilled bridges;
3. Counterexamples;
4. Reasons for failure;
5. Candidate lemmas;
6. Literature sources;
7. Computational results;
8. Dependency graph;
9. Contamination risks;
10. Suggestions for the next round.

---

# 36. The Core Theoretical Judgment of This Document

This document proposes:

$$
\boxed{
\text{Mathematical research}
\neq
\text{One-time proof output}
}
$$

It is more likely:

$$
\boxed{
\text{Continuous updating of the research state}
}
$$

Therefore:

$$
\mathcal S_t
\rightarrow
\mathcal S_{t+1}
$$

is the true core of an autonomous research Agent.

---

# 37. Conclusion

This document proposes a preliminary architecture for an autonomous mathematical research Agent that has not yet achieved generalized proof and has not yet been fully implemented.

Its core consists of three parts:

$$
\boxed{
\mathrm{RIITG}
}
$$

Responsible for reversely generating intermediate propositions from the result;

$$
\boxed{
\mathrm{RAB}
}
$$

Responsible for downgrading and backfilling transient bridges;

$$
\boxed{
\mathrm{KCPE}
}
$$

Responsible for executing local quasi-enumeration under the conditions of knowledge, failures, semantic windows, and computational budgets.

Together, these three form:

$$
\boxed{
\mathrm{AMRAL}
}
$$

Namely, the Autonomous Mathematical Research Agent Loop.

The complete dynamic is:

$$
\text{Analyze}
\rightarrow
\text{Generate}
\rightarrow
\text{Enumerate}
\rightarrow
\text{Retrieve}
\rightarrow
\text{Backfill}
\rightarrow
\text{Compute}
\rightarrow
\text{Verify}
\rightarrow
\text{Falsify}
\rightarrow
\text{Update}.
$$

This document does not claim that:

$$
\mathrm{AMRAL}
$$

has been proven effective.

This document only argues:

> From the perspective of theoretical structure, existing Agent capabilities, search, retrieval, computation, formal verification, and multi-agent parallelism, this architecture possesses implementable feasibility.

What truly requires subsequent proof and experimentation is:

1. Whether it can stably reduce the search space;
2. Whether it can increase the rate of effective intermediate propositions;
3. Whether it can reduce repeated failures;
4. Whether it can increase the discovery rate of new lemmas;
5. Whether it can outperform baselines in low-contamination blind tests.

Therefore, the ultimate positioning of this document is:

$$
\boxed{
\text{Implementable theoretical candidate architecture}
}
$$

Rather than:

$$
\boxed{
\text{Proven universal mathematical research system}
}
$$

However, if some of these propositions are supported in the future, autonomous mathematical Agents may no longer merely:

> Solve a single problem.

But rather:

> Continuously research a problem until the problem itself, the knowledge base space, the candidate proof graph, and the computational results co-evolve.

This is also the true long-term direction proposed by this document:

$$
\boxed{
\text{Research is dynamic computation;
Computation is continuous approximation.}
}
$$

---

# Appendix A: Minimal Formalization

## A.1 Research State

$$
\mathcal S_t
=
(
P_t,
\mathcal K_t,
\mathcal M_t,
\mathcal T_t,
\Omega_t,
\mathcal F_t,
\mathcal C_t,
\mathcal D_t
).
$$

---

## A.2 RIITG

$$
P_t
\rightsquigarrow
\mathcal M_t.
$$

---

## A.3 RAB

$$
\mathcal T_t
\Rightarrow
\mathcal M_t.
$$

---

## A.4 KCPE

$$
\Omega_t
=
\Omega(
P_t,
\mathcal K_t,
\mathcal F_{<t},
W_{\mathrm{sem}},
B_t
).
$$

---

## A.5 Knowledge Expansion

$$
\mathcal K_{t+1}
=
\mathcal K_t
\cup
\operatorname{Retrieve}(
G_t
).
$$

---

## A.6 State Update

$$
\mathcal S_{t+1}
=
\mathcal U(
\mathcal S_t,
\mathcal F_t,
\mathcal C_t,
\mathcal K_{t+1}
).
$$

---

# Appendix B: Method State Markers

- **K**: Known
- **P**: Provisional
- **C**: Conjectural
- **F**: Filled
- **R**: Refuted
- **S**: Structurally Useful
- **E**: Equivalent Risk
- **D**: Dependency Risk
- **X**: Contamination Risk

---

# Appendix C: Research Integrity Statement

1. The architecture in this document has not yet been proven to yield generalized gains.
2. This document has not yet completed a full implementation of the AMRAL system.
3. This document does not claim that autonomous Agents can already independently solve open mathematical problems.
4. All benefits in this document are propositions awaiting verification.
5. Any unproven bridge must not be written as a theorem.
6. Any web data must not be automatically deemed true.
7. Any finite computation must not masquerade as an infinite proof.
8. Any claims of novelty require post hoc literature auditing.
9. If future large-scale experiments do not support this method, the failed results should be publicly retained.
10. This document is positioned as a first draft and an implementable research architecture.

---

# Appendix D: Relationship with the Previous Three Papers

This document can be viewed as the fourth-layer extension of the three preceding research papers:

1. **Erroneous Generation Preservation Layer**  
   Retains the structural value within errors.

2. **Proof Engineering Layer**  
   Establishes RIITG and RAB.

3. **Experimental Auditing Layer**  
   Establishes quasi-blind testing, contamination control, and proof engineering observability.

4. **Autonomous Research Agent Layer**  
   This document proposes AMRAL and KCPE, transforming the methods into an iteratively executable Agent research loop.