Methodology

Starting point — a throwaway attempt at "inventing new number theory to prove the Riemann Hypothesis" produced five plausible-looking self-invented axioms. Rather than discarding them as junk or accepting them as genuine axioms, the three papers reposition them: every self-invented axiom is not a permanent premise but a transient bridging proposition — induced in reverse from the target result, which must then be demoted to a proof obligation and have its genuine foundations sought and backfilled term by term. The operation of "first inventing enough of a world, then proving that world holds" is what these three papers are actually studying.

RIITG (Result-Induced Intermediate Theorem Generation) — given a target proposition P, instead of searching directly for a proof of P, it generates in reverse a set of candidate intermediate propositions M: "if what held, would make P almost automatically true?" This is a search operator, not an inference rule — candidate propositions need not already exist in the current knowledge base.

RAB (Reverse Axiom Backfilling) — every candidate M is immediately demoted to a proof obligation; it is not allowed to sit as "provisionally true." A more basic support T is then sought, such that T⟹M. The whole process is bound by five ground rules: sufficiency (the conjunction of candidates must be able to derive P), non-circularity (P cannot be its own ancestor), backfillability (some T must genuinely exist), decreasing burden (proving M must be easier than proving P), and controllable semantic breadth.

Mesoscale semantic window — if the candidate space is too wide, it combinatorially explodes; too narrow, and the correct path may be deleted before the search even begins. All three papers consistently argue: effective intermediate propositions fall in a controllable range between the two, not "the more specific the better."

KCPE (Knowledge-Conditioned Proof-Space Enumeration) — not an enumeration of every possible proof, but a dynamic construction of a local candidate space Ω_t based on current knowledge, failure history, the semantic window, and the computational budget. Web search here is not "looking up the answer," but an expansion operator on the base knowledge space: triggered only when a clear gap is found, with the expanded knowledge fed back into candidate generation.

AMRAL (Autonomous Mathematical Research Agent Loop) — wraps the three above into a repeatable nine-step loop: analyze, generate, enumerate, retrieve, backfill, compute, verify, refute, update. The core stance is to model mathematical research itself as a dynamical system over research states (S_t → S_t+1), rather than a one-shot proof output; dividing labor across multiple agent roles (bridge generation, counterexample search, dependency auditing, ...) lets different intermediate propositions be attacked in parallel.

What isn't claimed — all three papers state plainly in their appendices: every benefit above is still to be verified, with no general proof. An unbackfilled bridge must not be written up as a theorem; finite computation must not masquerade as infinite proof; content retrieved from the web is not automatically treated as true. The Riemann Hypothesis case genuinely ran a round on this path — and did not prove the conjecture; the process data is on the Riemann Hypothesis page.