# Result-Induced Intermediate Theorem Generation and Reverse Axiom Backfilling

## ——A Bidirectional Proof Engineering Methodology: Reverse Generation of Proof Nodes from Targets and Forward Backfilling from Foundations

**Authors: Neo.K (Theoretical Conception) / Aletheia (Collaboration & Formalization)**  
**Version: v1.0 (General Methodology Draft)**  
**Date: 2026-07-09**

---

## Abstract

This paper proposes two coupled methodologies: **Result-Induced Intermediate Theorem Generation (RIITG)** and **Reverse Axiom Backfilling (RAB)**. The former starts from a known or to-be-proved target proposition and reversely generates a set of intermediate propositions that, if true, are sufficient to support the target. The latter demotes these intermediate propositions from "transient axioms" to "proof obligations," and then seeks more fundamental theorems, lemmas, constructions, invariants, estimates, operators, or local conditions to backfill them layer by layer. Its core structure is not a unidirectional derivation from premises to conclusions, but rather the establishment of two causal chains in opposite directions:

$$
P
\rightsquigarrow
M
\rightsquigarrow
T
$$

as the generative direction, and:

$$
T
\rightarrow
M
\rightarrow
P
$$

as the proof direction.

Here, $P$ is the target proposition, $M$ is the set of candidate intermediate propositions, and $T$ represents the more fundamental provable supports. This paper refers to this as the **reverse coupling of generative causality and proof causality**. The reversal here is not a strict inverse mapping in the functional sense, but a bidirectional engineering relationship in proof search and theory construction.

The primary question addressed in this paper is: How do we avoid the trivialization and pseudo-proofs associated with the notion that "any proposition can be proved as long as a sufficiently strong axiom is invented"? To this end, this paper establishes a complete set of constraints, including: sufficiency checks, acyclicity checks, proof burden reduction, semantic width control, candidate branch pruning, failure witnesses, dependency graphs, bridge minimization, alternative path comparison, target information leakage control, and post-hoc blind testing. This paper further proposes the **mesoscale semantic window**: the semantics of an intermediate proposition cannot be too wide, otherwise candidate solutions will face combinatorial explosion; nor can it be too narrow, otherwise the true proof path might be eliminated before the search even begins. Thus, an effective method does not seek the minimal semantic domain, but rather a controllable interval located between:

$$
W_{\min}
<
W_{\mathrm{sem}}
<
W_{\max}
$$

This paper also divides the methodology into three levels: the result-induced layer, the transient bridge layer, and the backfill proof layer, proposing a standard workflow suitable for human, AI, or human-AI collaborative use. This workflow includes: target normalization, reverse generation of sufficient conditions, bridge role annotation, semantic narrowing, dependency decyclization, proof burden estimation, local backfilling, hypergraph search, failure feedback, and path reconstruction. This paper argues that RIITG and RAB should not be viewed as new logical calculus rules, but rather positioned as a **proof engineering and theory discovery methodology**: they do not create truth, but reorganize the search space of "what to prove" and "what to prove first."

Finally, this paper proposes several testable propositions: whether intermediate proposition decomposition can reduce the maximum local proof burden; whether missing nodes non-trivially increase candidate explosion; whether the reverse coupling of generative and proof directions can improve the discovery rate of new lemmas; and whether AI can outperform proof search systems that only make binary true/false judgments by retaining the structural value in erroneous generations. These propositions will be verified in a subsequent third paper focusing on targeted experiments.

**Keywords:** Result-induction, intermediate theorem, reverse axiom backfilling, proof engineering, AI mathematical reasoning, lemma discovery, semantic width, candidate pruning, acyclicity, bidirectional search

---

# 1. Introduction

## 1.1 The Unidirectionality of Traditional Proof Narratives

A typical mathematical proof is often expressed as:

$$
A_1,A_2,\dots,A_n
\Rightarrow
P.
$$

Researchers start from known premises, definitions, and theorems, and step-by-step derive the target proposition $P$.

Abstractly written as:

$$
T_0
\rightarrow
T_1
\rightarrow
T_2
\rightarrow
\cdots
\rightarrow
P.
$$

This kind of narrative is very natural after a proof is completed, because a formal proof must unfold along a valid direction of inference.

However, **the discovery process of a proof** need not equate to the presentation order of the proof.

Researchers often know beforehand:

- What they want to achieve;
- Which conclusion, if true, would be sufficient;
- Which structure, if it exists, would suddenly simplify the problem;
- Which "unproven bridge," once established, would close the entire proposition.

Therefore, the discovery process might actually be:

$$
P
\rightsquigarrow
M_1
\rightsquigarrow
M_2
\rightsquigarrow
T,
$$

while the formal proof reverses this to:

$$
T
\rightarrow
M_2
\rightarrow
M_1
\rightarrow
P.
$$

This paper departs from this exact discrepancy.

---

## 1.2 Two Core Methods

This paper proposes:

### Method 1: Result-Induced Intermediate Theorem Generation

English:

**Result-Induced Intermediate Theorem Generation**

Abbreviation:

$$
\mathrm{RIITG}.
$$

Its task is:

> To reversely generate a set of intermediate propositions $M_i$ from the target proposition $P$ that might be sufficient to support $P$.

Formally:

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

where:

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

---

### Method 2: Reverse Axiom Backfilling

English:

**Reverse Axiom Backfilling**

Abbreviation:

$$
\mathrm{RAB}.
$$

Its task is:

> To demote intermediate propositions—temporarily treated as "sufficient if true"—into proof obligations, and then seek more fundamental supports.

Formally:

$$
\mathcal T
\overset{\mathrm{RAB}}{\Rightarrow}
\mathcal M
\Rightarrow
P.
$$

where:

$$
\mathcal T
=
\{T_1,\dots,T_m\}
$$

is a set of existing theorems, new lemmas, constructions, estimates, or lower-level propositions.

---

# 2. Core Intuition: First Invent a Sufficient World, Then Prove That World Holds

## 2.1 The Most Crude Form

Given a target:

$$
P.
$$

First assume there exists:

$$
A_1,\dots,A_n
$$

such that:

$$
A_1\land\cdots\land A_n
\Rightarrow
P.
$$

If we stop here, the method has no value, because one could simply choose:

$$
A_1=P.
$$

Or even:

$$
A_1:=\text{"$P$ is true"}.
$$

Therefore, the key to the method's validity is not "generating sufficient conditions," but rather:

1. The sufficient conditions cannot be identical to the target;
2. The sufficient conditions must be independently attackable;
3. The sufficient conditions should have a smaller or more localized proof burden;
4. Their proof dependencies must not return via the target itself.

---

## 2.2 Transient Axioms

This paper defines:

> A **transient axiom** is not an axiom permanently added to a formal system, but a candidate node temporarily assumed to be true during a proof search to test whether a certain chain of results closes.

Denoted as:

$$
A_i^{\ast}.
$$

Its lifecycle is:

$$
\text{Generation}
\rightarrow
\text{Sufficiency Check}
\rightarrow
\text{Demotion}
\rightarrow
\text{Backfilling}
\rightarrow
\text{Retention or Elimination}.
$$

If:

$$
A_i^{\ast}
$$

cannot be backfilled, it must not appear in the final proof.

---

# 3. Formal Framework

## 3.1 Proposition Space

Let:

$$
\mathfrak P
$$

be the space of all candidate propositions.

Target:

$$
P\in\mathfrak P.
$$

Intermediate set:

$$
\mathcal M
\subset
\mathfrak P.
$$

Support set:

$$
\mathcal T
\subset
\mathfrak P.
$$

---

## 3.2 Generation Operator

Define the result-induced generation operator:

$$
\mathcal R:
\mathfrak P
\rightarrow
2^{\mathfrak P}.
$$

where:

$$
\mathcal R(P)
=
\{M_1,\dots,M_n\}.
$$

Note:

$$
M_i\in\mathcal R(P)
$$

does not mean:

$$
P\Rightarrow M_i.
$$

It only means:

> Based on $P$'s structure, negation form, boundary conditions, symmetries, known necessary conditions, counterexample shapes, and candidate representations, $M_i$ is generated as a potential bridge.

Therefore:

$$
\mathcal R
$$

is a search operator, not an inference rule.

---

## 3.3 Backfilling Operator

Define the backfilling operator:

$$
\mathcal B:
\mathfrak P
\rightarrow
2^{\mathfrak P}.
$$

where:

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

represents candidate supports.

If it can be proved that:

$$
T_{i1}\land\cdots\land T_{ik}
\Rightarrow
M_i,
$$

then a local backfill is completed.

---

## 3.4 Complete Structure

Ideal state:

$$
P
\overset{\mathcal R}{\rightsquigarrow}
\mathcal M,
$$

then:

$$
\mathcal T
\overset{\mathcal B}{\Rightarrow}
\mathcal M,
$$

and:

$$
\bigwedge_{M\in\mathcal M}M
\Rightarrow
P.
$$

Therefore:

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

---

# 4. Generative Causality and Proof Causality

## 4.1 Generative Direction

The researcher first sees the target:

$$
P.
$$

Then asks:

> What, if true, would make $P$ almost automatically true?

Yielding:

$$
M.
$$

Then asks:

> What more fundamental condition, if true, would make $M$ true?

Yielding:

$$
T.
$$

Thus:

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

---

## 4.2 Proof Direction

A truly valid proof must go in reverse:

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

---

## 4.3 Reverse Coupling

This paper proposes:

$$
\boxed{
\mathcal C_{\mathrm{gen}}
\approx
\mathcal C_{\mathrm{proof}}^{-1}
}
$$

where:

- $\mathcal C_{\mathrm{gen}}$ : Generative causality;
- $\mathcal C_{\mathrm{proof}}$ : Proof causality.

The symbol:

$$
\approx
$$

denotes a structural correspondence, not a strict algebraic inverse.

The core here is:

> Results determine "where to look," foundations determine "whether it holds."

---

# 5. RIITG Phase 1: Target Normalization

## 5.1 Why We Cannot Generate Directly from Natural Language Targets

If the target is written as:

> Prove that a certain system is always stable.

The term "stable" might have multiple definitions.

Therefore, first normalize the target:

$$
P
=
Q_1x_1
Q_2x_2
\cdots
Q_kx_k
:
\Phi(x_1,\dots,x_k).
$$

where:

- $Q_i$ are quantifiers;
- $\Phi$ is an explicit predicate.

---

## 5.2 Simultaneous Generation of Negation

If:

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

then:

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

RIITG not only generates intermediate propositions from $P$, but also generates counterexample shapes from:

$$
\neg P
$$

This is crucial because many effective bridges come from asking:

> If $P$ fails, what kind of observable witness must appear?

---

# 6. RIITG Phase 2: Bridge Role Generation

This paper suggests that intermediate propositions should be generated from at least the following role categories.

## 6.1 Representation Bridge

Transform the original problem into another representation:

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

For example:

- Graphs to complexes;
- Sequences to generating functions;
- Geometric problems to operator problems;
- Combinatorial problems to topological invariants.

---

## 6.2 Exclusive Bridge

Find:

$$
\neg P
\Rightarrow
W,
$$

where $W$ is a counterexample witness.

Then prove:

$$
W
\Rightarrow
\bot.
$$

---

## 6.3 Positivity Bridge

Transform the target into:

$$
P
\iff
\forall f,\ Q(f)\ge0.
$$

Or:

$$
P
\Leftarrow
\forall f,\ Q(f)\ge0.
$$

---

## 6.4 Invariant Bridge

Find:

$$
I(X)
$$

such that:

$$
\neg P
\Rightarrow
I(X)\neq c,
$$

but separately establish:

$$
I(X)=c.
$$

---

## 6.5 Compression Bridge

Compress a massive counterexample space into:

$$
\mathcal G
\subset
\mathcal H.
$$

Requiring:

$$
\exists w\in\mathcal H\text{ is a counterexample}
\Rightarrow
\exists g\in\mathcal G\text{ is a counterexample}.
$$

---

## 6.6 Closure Bridge

If it has been proved on a generating family that:

$$
\forall g\in\mathcal G,\ P(g),
$$

then use:

$$
\overline{\mathcal G}=X
$$

and continuity to propagate the result to the universal set.

---

## 6.7 Local-Global Bridge

Decompose:

$$
G(X)
$$

into:

$$
G(X)
=
\sum_iL_i(X)
+
R(X).
$$

Then control the global via local estimates.

---

# 7. Standard Format of Transient Bridge Propositions

Every intermediate proposition $M_i$ must carry six fields.

## 7.1 Domain of Objects

$$
\operatorname{Dom}(M_i).
$$

---

## 7.2 Quantifier Structure

For example:

$$
\forall x\in X,\ \exists y\in Y.
$$

---

## 7.3 Conclusion Predicate

$$
\Psi_i(x,y).
$$

---

## 7.4 Failure Witness

There exists an explicit:

$$
w_i
$$

such that:

$$
w_i
\Rightarrow
\neg M_i.
$$

---

## 7.5 Expected Role

For example:

- Representation;
- Exclusive;
- Compression;
- Positivity;
- Closure;
- Estimate;
- Invariant.

---

## 7.6 Backfill Interface

List possible support types:

$$
\mathcal I(M_i)
=
\{
\text{Theorem},
\text{Lemma},
\text{Construction},
\text{Operator},
\text{Estimate},
\dots
\}.
$$

---

# 8. RAB: Reverse Axiom Backfilling

## 8.1 Step 1: First Check Sufficiency

For the candidate set:

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

one must first verify:

$$
\bigwedge_iM_i
\Rightarrow
P.
$$

If not, then:

$$
\mathcal M
$$

is not a complete bridge set.

---

## 8.2 Step 2: Demote All

It is forbidden to permanently retain:

$$
M_i
$$

as a "new axiom."

Uniformly change to:

$$
M_i\in\mathcal O,
$$

where $\mathcal O$ stands for proof obligations.

---

## 8.3 Step 3: Generate Support Candidates Item by Item

For each:

$$
M_i,
$$

generate:

$$
\mathcal B(M_i)
=
\{T_{i1}^{(1)},T_{i1}^{(2)},\dots\}.
$$

---

## 8.4 Step 4: Build Dependency Graph

Let:

$$
\mathcal D
=
(V,E).
$$

where:

- $V$ : Propositions;
- $E$ : Implication dependencies.

If:

$$
T\rightarrow M,
$$

then there is an edge:

$$
T\to M.
$$

---

## 8.5 Step 5: Decyclization

If:

$$
P
\leadsto
M_i
$$

appears in the proof dependency ancestors, then:

$$
M_i
$$

might be circular.

Require:

$$
P
\notin
\operatorname{Anc}(M_i).
$$

---

# 9. Acyclicity

## 9.1 Direct Cycle

$$
P\Rightarrow M
$$

and:

$$
M\Rightarrow P.
$$

If proving $M$ uses $P$, it is invalid.

---

## 9.2 Equivalence Disguise

If:

$$
M\iff P,
$$

then $M$ is not necessarily valueless, but one cannot claim it reduces the difficulty.

---

## 9.3 Definitional Smuggling

Forbidden:

$$
M:=\{x:P(x)\}.
$$

And then deriving from the definition:

$$
P.
$$

---

## 9.4 Numerical or Experimental Smuggling

If the target is an infinite proposition, finite verification must not be directly treated as a backfill.

---

# 10. Proof Burden

## 10.1 Why Decomposition is Not Always Valuable

If:

$$
P
$$

is very difficult,

but after generating:

$$
M_1,\dots,M_n
$$

each is equally difficult, then the method merely increases the workload.

---

## 10.2 Local Maximum Burden

Define a rough proof burden:

$$
C(P).
$$

Ideal situation:

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

---

## 10.3 Total Burden

One could also consider:

$$
C_{\mathrm{sum}}
=
\sum_iC(M_i).
$$

But the sum is not the sole criterion.

If they can be processed in parallel, then:

$$
C_{\mathrm{parallel}}
\approx
\max_iC(M_i).
$$

This is especially important for AI multi-agent systems.

---

## 10.4 Burden Reduction Ratio

Define:

$$
R_C
=
\frac{C(P)}
{\max_iC(M_i)}.
$$

If:

$$
R_C>1,
$$

it indicates a decrease in the maximum local burden.

---

# 11. Semantic Width

## 11.1 Number of Candidates

For each $M_i$, assume the number of reasonable formalization candidates is:

$$
N_i.
$$

Then:

$$
|\Omega|
\approx
\prod_iN_i.
$$

---

## 11.2 Semantic Width

Define:

$$
W_{\mathrm{sem}}
=
\sum_i\log N_i.
$$

---

## 11.3 Too Wide

If:

$$
W_{\mathrm{sem}}\gg1,
$$

then candidates explode.

---

## 11.4 Too Narrow

If:

$$
W_{\mathrm{sem}}\to0,
$$

it might prematurely exclude the true path.

---

## 11.5 Mesoscale Window

Propose:

$$
\boxed{
W_{\min}
<
W_{\mathrm{sem}}
<
W_{\max}
}
$$

as the effective search region.

---

# 12. Missing Nodes and Candidate Explosion

This paper proposes:

> Too many candidates and incomplete intermediate propositions might be two manifestations of the same underlying problem.

Assume proposition $M$ is missing:

- Domain of objects;
- Quantifiers;
- Mappings;
- Invariants;
- Failure conditions.

Then every missing field generates a bifurcation.

If the $j$-th missing field has:

$$
k_j
$$

reasonable candidates, then:

$$
N(M)
\approx
\prod_jk_j.
$$

Therefore:

$$
I(M)\downarrow
\Rightarrow
N(M)\uparrow,
$$

where:

- $I(M)$ : Completeness;
- $N(M)$ : Number of formalization candidates.

---

# 13. Candidate Pruning

## 13.1 Type Pruning

If the target object is a graph, candidate bridges can cross domains, but new objects must specify a mapping:

$$
F:G\mapsto X.
$$

Pure analogies without mappings are eliminated.

---

## 13.2 Quantifier Pruning

If a candidate secretly changes:

$$
\forall x
$$

to:

$$
\exists x,
$$

unless it can be proven sufficient, it is eliminated.

---

## 13.3 Counterexample Pruning

If a known counterexample directly negates $M_i$, it is eliminated.

---

## 13.4 Cycle Pruning

If:

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

eliminate or flag as circular.

---

## 13.5 Burden Pruning

If it is estimated that:

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

and there are no other structural benefits, lower its priority.

---

# 14. Minimal Bridge Set

If:

$$
\mathcal M
$$

is sufficient to derive $P$,

search for a minimal subset:

$$
\mathcal M^\ast
\subseteq
\mathcal M
$$

such that:

$$
\bigwedge_{M\in\mathcal M^\ast}M
\Rightarrow
P.
$$

And require:

$$
\forall M_j\in\mathcal M^\ast,
$$

we have:

$$
\bigwedge_{M\in\mathcal M^\ast\setminus\{M_j\}}M
\not\Rightarrow
P.
$$

This is bridge minimization.

---

# 15. Proof Hypergraph

A standard dependency graph only expresses:

$$
A\to B.
$$

But mathematics often requires joint premises:

$$
A\land B\Rightarrow C.
$$

Therefore, define a proof hypergraph:

$$
\mathfrak G
=
(V,\mathcal E).
$$

Hyperedge:

$$
\{A,B\}
\rightarrow
C.
$$

RIITG generates candidate intermediate nodes.

RAB searches for hyperedges to backfill.

---

# 16. Failure Feedback

If a certain bridge:

$$
M_i
$$

fails, one should not directly restart the entire search.

First classify:

## 16.1 Proposition is False

Found:

$$
w_i\Rightarrow\neg M_i.
$$

---

## 16.2 Proposition is Too Strong

Might weaken:

$$
M_i
\rightarrow
M_i'.
$$

---

## 16.3 Proposition is Too Weak

Although provable, but:

$$
M_i
\not\Rightarrow
\text{required bridge function}.
$$

---

## 16.4 Semantics Incomplete

Needs to supplement:

$$
G_i.
$$

---

## 16.5 Domain Incompatible

$$
\operatorname{Dom}(M_i)
\cap
\operatorname{Dom}(M_j)
=
\varnothing.
$$

---

# 17. Dynamic Reconstruction

Define the intermediate set at round $t$:

$$
\mathcal M_t.
$$

After failure:

$$
\mathcal M_{t+1}
=
\mathcal U(
\mathcal M_t,
\mathcal F_t
),
$$

where:

- $\mathcal F_t$ : Failure information;
- $\mathcal U$ : Update operator.

Thus the method is not a one-time generation, but:

$$
\mathcal M_0
\rightarrow
\mathcal M_1
\rightarrow
\cdots
\rightarrow
\mathcal M_t.
$$

---

# 18. Human and AI Role Division

## 18.1 AI's Advantages

AI is suited for:

- Generating intermediate propositions in bulk;
- Cross-domain mapping;
- Formal rewriting;
- Searching for candidate equivalent representations;
- Building dependency graphs;
- Counterexample searching;
- Multi-agent parallel backfilling.

---

## 18.2 AI's Risks

AI is prone to:

- Inventing empty-shell terminology;
- Smuggling the target;
- Substituting logical implication with semantic similarity;
- Generating cycles;
- Deleting valuable structures along with errors during correction.

---

## 18.3 Three-Valued Evaluation

Therefore, we recommend:

$$
\{
\text{valid},
\text{invalid},
\text{structurally-useful}
\}.
$$

Instead of:

$$
\{
\text{correct},
\text{garbage}
\}.
$$

---

# 19. AI Execution Protocol

## Phase 0: Target Isolation

Input:

$$
P.
$$

Reading the standard proof is forbidden.

---

## Phase 1: Target Normalization

Output:

- Quantifiers;
- Domain of objects;
- Negation form;
- Counterexample shape.

---

## Phase 2: Role-Based Generation

Require AI to separately generate:

- Representation bridges;
- Exclusive bridges;
- Invariant bridges;
- Positivity bridges;
- Compression bridges;
- Closure bridges.

---

## Phase 3: Semantic Narrowing

Fill out six fields for each proposition.

---

## Phase 4: Sufficiency Verification

Check:

$$
\mathcal M\Rightarrow P.
$$

---

## Phase 5: Bridge Minimization

Find:

$$
\mathcal M^\ast.
$$

---

## Phase 6: Demote All

Mark:

$$
M_i\in\mathcal O.
$$

---

## Phase 7: Backfill Generation

For each $M_i$, search for:

$$
T_{ij}.
$$

---

## Phase 8: Decyclization

Build:

$$
\mathfrak G_{\mathrm{proof}}.
$$

---

## Phase 9: Counterexample and Failure Testing

Actively search for:

$$
\neg M_i.
$$

---

## Phase 10: Blind Test Comparison

Compare with the known proof only at the very end.

---

# 20. Pseudocode

```text
INPUT:
    Target proposition P
    Allowed semantic universe U
    Candidate budget B
    Max semantic width W_max

STEP 1:
    Normalize P
    Construct not-P
    Extract witnesses and structural signatures

STEP 2:
    Generate candidate bridge propositions M
    Label each M by bridge role

STEP 3:
    Formalize:
        domain
        quantifiers
        predicate
        failure witness
        expected function
        backfill interface

STEP 4:
    Remove candidates that:
        leak P
        are circular
        are undefined
        exceed semantic width
        are refuted by known counterexamples

STEP 5:
    Search for subsets M*
    such that M* => P

STEP 6:
    Minimize M*

STEP 7:
    Demote every M in M*
    to proof obligation

STEP 8:
    For each M:
        generate supports T
        test T => M
        build dependency hypergraph

STEP 9:
    Reject paths where P appears in ancestors

STEP 10:
    Estimate proof burden

STEP 11:
    If some M fails:
        classify failure
        weaken, split, replace, or add missing node

STEP 12:
    Repeat until:
        proof closes
        search budget exhausted
        semantic width explodes
        or bridge family is falsified

OUTPUT:
    closed proof path
    or structured failure report
```

---

# 21. Minimum Conditions for Method Validity

## 21.1 Sufficiency

$$
\bigwedge_iM_i
\Rightarrow
P.
$$

---

## 21.2 Acyclicity

$$
P
\notin
\operatorname{Anc}(M_i).
$$

---

## 21.3 Backfillability

For at least some $M_i$, there exists:

$$
\mathcal T_i
\Rightarrow
M_i.
$$

---

## 21.4 Burden Reduction

Ideal:

$$
\max_iC(M_i)
<
C(P).
$$

---

## 21.5 Branch Controllability

$$
W_{\mathrm{sem}}
<
W_{\max}.
$$

---

# 22. Differences from Other Reasoning Methods

## 22.1 Difference from Standard Backward Chaining

Backward chaining typically searches for the antecedents of known rules starting from the target.

RIITG allows the generation of:

$$
\text{new intermediate propositions not yet existing in the knowledge base}.
$$

Therefore:

$$
\text{retrieval}
\neq
\text{generation}.
$$

---

## 22.2 Difference from Lemma Guessing

Traditional lemma discovery usually searches for auxiliary propositions within an established formal system.

RIITG places more emphasis on:

- Reverse induction from results;
- Cross-representation capability;
- Ability to generate new objects;
- The need to control semantic width.

---

## 22.3 Difference from Abductive Reasoning

Abductive reasoning asks:

> What cause best explains the observation?

RIITG asks:

> What intermediate structure, if true, best makes the target proposition provable?

The two are similar, but the goals are different.

---

## 22.4 Difference from Axiomatization

RAB discourages permanently adding axioms.

Instead:

$$
\text{Transient Axiom}
\rightarrow
\text{Proof Obligation}.
$$

---

# 23. Methodological Propositions

The following are all propositions to be verified, not proven theorems.

## Proposition 1: Intermediate Maximum Burden Reduction Proposition

There exists a problem class $\mathcal C$ such that for some:

$$
P\in\mathcal C,
$$

RIITG can generate:

$$
M_1,\dots,M_n
$$

satisfying:

$$
\max_iC(M_i)
<
C(P).
$$

---

## Proposition 2: Missing Node Explosion Proposition

If the completeness of an intermediate proposition decreases:

$$
I(M)\downarrow,
$$

then the expected number of reasonable formalization candidates increases:

$$
\mathbb E[N(M)]\uparrow.
$$

---

## Proposition 3: Reverse Coupling Gain Proposition

Bidirectional search:

$$
P
\rightsquigarrow
M
\leftarrow
T
$$

on certain problem classes is more likely to discover non-trivial intermediate lemmas than unidirectional search:

$$
T\rightarrow\cdots\rightarrow P
$$

---

## Proposition 4: Structure Preservation Proposition

The three-valued evaluation:

$$
\{
V,I,S
\}
$$

where $S$ stands for structurally useful,

in AI theory discovery tasks, may retain more candidates that can be successfully formalized later than the binary evaluation:

$$
\{V,I\}
$$

---

## Proposition 5: Mesoscale Semantic Window Proposition

There exist certain problems such that the search success rate:

$$
R(W_{\mathrm{sem}})
$$

is not a monotonic function, but has a higher value in the intermediate region:

$$
\exists W^\ast:
R(W^\ast)
>
R(W_{\min}),
R(W_{\max}).
$$

---

# 24. Falsifiability

A methodology must allow for failure.

## 24.1 If Blind Tests Yield No Gain

If RIITG on multiple known difficult propositions:

- Cannot generate effective bridges;
- Only restates the conclusion;
- Has a low backfill rate;
- Incurs search costs higher than the baseline;

then the method is falsified.

---

## 24.2 If the Semantic Window Does Not Exist

If the success rate has no stable relationship with:

$$
W_{\mathrm{sem}}
$$

then the mesoscale window proposition fails.

---

## 24.3 If Three-Valued Evaluation is Invalid

If structurally useful candidates do not have a higher ultimate formalization success rate than random erroneous candidates, then this proposition fails.

---

# 25. Experimental Design Principles

Formal testing should not prioritize completely open hard problems.

One should select problems that are:

1. Known to be true;
2. Non-trivial to prove;
3. Whose standard proofs can be hidden;
4. Have multiple paths;
5. Allow for post-hoc comparison.

---

# 26. Evaluation Metrics

## 26.1 Effective Bridge Rate

$$
R_{\mathrm{bridge}}
=
\frac{
\#\text{provable and useful bridges}
}{
\#\text{generated bridges}
}.
$$

---

## 26.2 Backfill Rate

$$
R_{\mathrm{fill}}
=
\frac{
\#\text{successfully backfilled propositions}
}{
\#\text{propositions to be backfilled}
}.
$$

---

## 26.3 Novel Path Rate

$$
R_{\mathrm{novel}}
=
\frac{
\#\text{paths non-isomorphic to the standard proof}
}{
\#\text{successful paths}
}.
$$

---

## 26.4 Cycle Rate

$$
R_{\mathrm{circ}}
=
\frac{
\#\text{circular candidates}
}{
\#\text{total candidates}
}.
$$

---

## 26.5 Candidate Explosion Rate

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

---

# 27. Three Possible Outcomes

## 27.1 Complete Success

Obtain:

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

---

## 27.2 Partial Success

$P$ is not completed, but a new lemma is obtained:

$$
T^\ast.
$$

---

## 27.3 Structural Failure

Prove that a certain class of intermediate paths is impossible.

This still has value because it narrows the search domain.

---

# 28. Separation of Theory Discovery and Proof

This paper advocates a clear distinction between:

$$
\text{Discovery}
$$

and:

$$
\text{Justification}.
$$

RIITG primarily serves:

$$
\text{Discovery}.
$$

RAB is responsible for sending candidates into:

$$
\text{Justification}.
$$

Therefore:

$$
\text{Generated well}
\not\Rightarrow
\text{Proof holds}.
$$

However:

$$
\text{Generation failure}
$$

should also not merely be understood as an "error," but potentially as a structure awaiting formalization.

---

# 29. Generalization to Non-Mathematical Fields

Although this paper centers on proof engineering, the method can be abstracted to other fields.

## 29.1 Scientific Theories

Target phenomenon:

$$
P.
$$

Generate:

$$
M_i
$$

as intermediate mechanisms.

Then backfill via:

$$
T_j
$$

---

## 29.2 Program Verification

Target specification:

$$
P.
$$

Generate loop invariants:

$$
M_i.
$$

Then prove:

$$
T_j\Rightarrow M_i.
$$

---

## 29.3 Causal Modeling

Target:

$$
Y.
$$

Generate candidate mediators:

$$
M.
$$

Then verify:

$$
X\rightarrow M\rightarrow Y.
$$

---

# 30. Risks and Ethics

## 30.1 Pseudo-Proof Generation

AI might generate a massive amount of seemingly beautiful bridges.

---

## 30.2 Illusion of Authority

Formalized symbols do not equate to a proof.

## 30.3 Open Problem False Alarms

Any un-backfilled bridge must not be written as a proven theorem.

---

## 30.4 Research Credit

The methods proposed by humans, candidates generated by AI, and checks completed by formal proof systems should have their contributions recorded separately.

---

# 31. Proposed Paper Tagging System

Tag each proposition:

- **K**: Known;
- **C**: Conjectural;
- **P**: Provisional;
- **R**: Refuted;
- **F**: Filled;
- **E**: Equivalent-risk;
- **D**: Dependency-risk.

For example:

$$
M_3[\mathrm{P,D}]
$$

indicates it is provisional and carries a dependency risk.

---

# 32. Final General Form

Given target:

$$
P.
$$

RIITG:

$$
P
\rightsquigarrow
\mathcal M_0.
$$

Semantic narrowing:

$$
\mathcal M_0
\rightarrow
\mathcal M_1.
$$

Sufficiency and minimization:

$$
\mathcal M_1
\rightarrow
\mathcal M^\ast.
$$

RAB:

$$
\mathcal T
\Rightarrow
\mathcal M^\ast.
$$

Finally:

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

If it fails:

$$
\mathcal F
\Rightarrow
\mathcal M^\ast
\mapsto
\mathcal M^{\ast\prime}.
$$

Then iterate.

---

# 33. Conclusion

This paper proposes two coupled methods:

$$
\mathrm{RIITG}
$$

and:

$$
\mathrm{RAB}.
$$

The former reversely generates intermediate propositions from the result:

$$
P
\rightsquigarrow
M.
$$

The latter forward-backfills from foundations:

$$
T
\rightarrow
M.
$$

Ultimately forming:

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

Its core does not lie in "allowing the creation of one's own axioms," but rather in:

$$
\boxed{
\text{Any self-created axiom must be demoted to a proof obligation}
}
$$

The true value of the method depends on:

- Whether it reduces the local maximum proof burden;
- Whether it controls semantic width;
- Whether it avoids cycles;
- Whether it can find a minimal bridge set;
- Whether it can produce backfillable intermediate theorems in blind tests.

This paper further proposes:

$$
\boxed{
\text{Generative Causality}
\approx
\text{Proof Causality}^{-1}
}
$$

as the core methodological proposition.

This is not a new logical truth, but a new proof engineering perspective.

The next step should be to use a proposition that is "known to be true but non-trivial to prove" as a blind test target, and record:

$$
R_{\mathrm{bridge}},
R_{\mathrm{fill}},
R_{\mathrm{circ}},
R_{\mathrm{branch}},
R_{\mathrm{novel}}.
$$

Only through such experiments can RIITG and RAB transition from a conceptual methodology into a verifiable research program.

---

# Appendix A: Minimal Definition Table

## A.1 RIITG

$$
\mathcal R(P)
=
\mathcal M.
$$

---

## A.2 RAB

$$
\mathcal B(M_i)
=
\mathcal T_i.
$$

---

## A.3 Sufficiency

$$
\bigwedge_iM_i
\Rightarrow
P.
$$

---

## A.4 Backfilling

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

---

## A.5 Acyclicity

$$
P
\notin
\operatorname{Anc}(M_i).
$$

---

## A.6 Semantic Width

$$
W_{\mathrm{sem}}
=
\sum_i\log N_i.
$$

---

## A.7 Candidate Space

$$
|\Omega|
\approx
\prod_iN_i.
$$

---

## A.8 Burden Reduction

$$
R_C
=
\frac{C(P)}
{\max_iC(M_i)}.
$$

---

# Appendix B: Standard Bridge Card

```text
Bridge ID:
Name:
Role:
Domain:
Quantifiers:
Formal Statement:
Why Sufficient:
Failure Witness:
Candidate Backfills:
Dependency Risks:
Equivalence Risk:
Semantic Width:
Estimated Proof Burden:
Status:
```

---

# Appendix C: AI Multi-Agent Division of Labor

## Agent 1: Target Normalizer

Outputs:

$$
P,\neg P.
$$

## Agent 2: Bridge Generator

Generates:

$$
\mathcal M.
$$

## Agent 3: Sufficiency Checker

Checks:

$$
\mathcal M\Rightarrow P.
$$

## Agent 4: Circularity Auditor

Builds dependency graph.

## Agent 5: Backfill Generator

Searches for:

$$
\mathcal T_i.
$$

## Agent 6: Counterexample Hunter

Searches for:

$$
\neg M_i.
$$

## Agent 7: Semantic Width Controller

Controls:

$$
W_{\mathrm{sem}}.
$$

## Agent 8: Proof Burden Estimator

Estimates:

$$
C(M_i).
$$

## Agent 9: Hypergraph Planner

Searches:

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

## Agent 10: Human Theorist

Decides:

- Which errors are worth retaining;
- Which cross-domain mappings have ontological significance;
- Which nodes are merely linguistic hallucinations;
- When to expand or narrow the semantic domain.

---

# Appendix D: Research Integrity Statement

1. RIITG is not a proof rule.
2. RAB does not allow unproven premises to enter the final proof.
3. Transient axioms must be demoted to proof obligations.
4. Any bridge equivalent to the target must be explicitly marked.
5. Any backfill path dependent on the target must be marked as circular.
6. New terminology generated by AI does not automatically possess mathematical content due to a formalized appearance.
7. Both successful and failed cases should be retained.
8. The validity of formal methods must be subjected to blind testing.

---

# Version Notes

This paper is the second in a sequence of three papers:

1. First paper: **"From Transient Axioms to Backfillable Bridges: Result-Induced Intermediate Proposition Reconstruction in the Case of the Riemann Hypothesis"**;
2. This paper: **"Result-Induced Intermediate Theorem Generation and Reverse Axiom Backfilling"**;
3. Next paper: **Targeted Experiment Paper — Blind Testing, Evaluation, and Falsification Procedures on Known but Non-Trivial Propositions.**