Recursive Reasoning Exploration: Mathematical Research through Evolving Reasoning Graphs : case study: An Exact Certificate-Degree Theorem for Two-Term Tensor Decompositions : Phase III of the Math Instruments Program

Ying Xie

cs.AINov 1, 2026

Recursive Reasoning Exploration: Mathematical Research through Evolving Reasoning Graphs : case study: An Exact Certificate-Degree Theorem for Two-Term Tensor Decompositions : Phase III of the Math Instruments Program

Authors: Ying Xie

Organizations: Kennesaw State University

Abstract

Large collections of manuscripts and research notes offer ways to reuse arguments, while making it harder to retain hypotheses, check claims, and understand how results were obtained. We propose Recursive Reasoning Exploration (RRE), a framework for cumulative mathematical research through evolving reasoning graphs. RRE links claims and jointly required premises to research targets, attempted arguments, counterexamples, checks, and revisions. Each investigation can generate further targets, and its supported outcomes become available to subsequent investigations. This is Phase III of the Math Instruments program: identifying mathematical instruments, reconstructing reusable reasoning, and organizing recursive research from that reasoning. The framework supports human-directed, collaborative, and goal-directed autonomous exploration, with open-ended exploration as a further mode. Its records also provide material for learning how mathematical investigations develop. A complexity research case study establishes an exact theorem: for every complex tensor of order n >= 2 and rank greater than two, the minimum Nullstellensatz certificate degree for its original two-term decomposition equations is 3n. This includes an infinite family whose every flattening has rank at most two. The exploration develops an explicit boundary certificate, a balanced transfer lemma, and an exhaustive argument using classical rank-two geometry. A parallel branch gives bounds 3m + 3 <= delta_m(I_m, N) <= 3m + 6 for every nonzero nilpotent m by m matrix. Six graph revisions record the progression from inherited results to these theorems, with exact arithmetic checks and a replayable exploration history. We present the RRE representation and protocol, the mathematical proofs, visualizations of graph evolution, and a research agenda for shared human-AI exploration, cumulative reuse, and education.

Figures & tables

Phase	Primary question	Main record	Next use
I	What mathematical device may be reusable?	Instrument, source, antecedents, caveats	Select mechanisms worth reconstructing
II	Why does it work, and under which hypotheses?	Reasoning graph with scope and transfer obligations	Find candidate routes and missing premises
III	What should be investigated next, and how does the outcome change what we know?	Evolving reasoning graph and exploration history	Reuse results and failures in subsequent research

Table 1: The phases describe a research program. They are not levels of verification: every phase needs its own mathematical review.

Operating mode	Objective formation and investigation
Human-directed exploration	Researchers choose and investigate questions, using the graph to organize their work.
Collaborative Reasoning Exploration	Humans and AI jointly formulate questions, investigate arguments, and extend the graph, with recorded contributions and handoffs.
Goal-directed autonomous exploration	A researcher supplies the overall objective; an AI agent recursively selects and investigates intermediate targets within the declared charter.
Open-ended autonomous exploration	An AI agent formulates research objectives from the collection and investigates them under standing evaluation and resource policies.

Table 2: Four operating modes of RRE. They describe the allocation of research activities, not levels of mathematical verification. The case study illustrates the third mode.

Mathematical status	Meaning in this paper
Source assertion	A statement faithfully attributed to a source; independent validity is not implied.
Conjecture	A proposed statement without an admitted proof.
Conditional derivation	An argument with named assumptions or unresolved premises still attached.
Proof recorded	A complete argument is supplied at its declared level of rigor; its review record remains separate.
Computation	An exact or numerical result for stated inputs or a finite range. It supports only the claim actually checked.
Refutation	A counterexample or argument contradicts a specified statement under the same hypotheses.

Table 3: Mathematical statuses. Supersession and withdrawal are revision states; they preserve the earlier record. A failed attempt is an event outcome, not a refutation.

Operation	Question generated	Admission obligation
Composition	Can one result supply a premise of another?	Align objects, scopes, and quantifiers
Transfer	Can a mechanism work in a different setting?	Prove the correspondence and missing bridge lemmas
Quantitative refinement	Can a bound meet the next theorem’s requirements?	Retain every growing parameter and cost
Generalization	Which assumption can be weakened?	Check the modified proof and boundary cases
Obstruction analysis	What condition avoids a counterexample?	State exactly what the counterexample rules out
Structural synthesis	Do several arguments express one reusable mechanism?	Separate analogy from a proved common statement

Table 4: Target-generation operations. They organize candidate questions; none guarantees a useful discovery.

Panel of Figure 1 — Figure 1: The proposed RRE cycle. Arrows describe research activity, not mathematical implication. Feedback may generate new targets and, in the open-ended mode, new overall objectives under the declared policy; it does not permit circular proofs. A stopping decision saves the state and remaining obligations.

Level	Description	Evidence needed for an achieved result
S0	Connection or recovery	A useful relationship or known result is correctly identified.
S1	Local advance	A stated subproblem is resolved in its required scope.
S2	Reusable advance	A method or result supports a documented class of further arguments.
S3	Major bottleneck closed	A predeclared major obstacle is resolved with the parameters needed downstream.
S4	Objective resolved	A complete argument establishes the primary objective at the stated review level.

Table 5: Significance is separate from proof status and literature novelty. A conjecture may have potential S3 significance without being an achieved S3 result.

Criterion	Required deliverable
1. Infinite family	A theorem beyond ordinary flattening tests, with explicit hypotheses and quantifiers in the original decomposition parameters.
2. Matching bounds	Matching lower and upper certificate-degree bounds, preferably exact. Matching asymptotics must provide a substantive advance in method and theorem.
3. Reusable method	A construction or lower-bound method with a proved extension or justified applicability class beyond one isolated tensor.
4. Literature comparison	A documented comparison with the closest tensor-rank and algebraic-proof-complexity results, distinguishing inherited ingredients from the new claims.
5. Replayable record	Full arguments, exact checks, source hashes, chronological decisions and failures, and before-and-after reasoning graphs.

Table 6: The five prospectively approved criteria for the case study’s completion milestone. Completion requires all five.

Revision	Nodes	AND steps	Mathematical or historical effect
v001	8	0	Fix the objective, raw model, inherited bounds, and boundary family.
v002	19	7	Establish complete symmetry reduction and exact degrees 9 and 12; generate a uniform target.
v003	43	22	Certify degree 15 and prove the all- $m$ pencil bound; generate the endpoint question.
v004	46	22	Add multiple-block screens and retain the remaining gap.
v005	66	33	Prove balanced transfer, the $W_{n}$ formula, and the all-target two-term theorem.
v006	68	34	Complete the mathematical audit, replay delivery, and milestone assessment.

Table 7: Saved graph states during the exploration. Counts include scopes, evidence, objectives, and open questions as well as derived claims.

Panel of Figure 2 — Figure 2: Recorded research progression. Each stage changes what the next investigation can use. Arrows describe exploration history, while the theorem’s implication structure is shown separately in figure 4 . The open pencil endpoint survives the success of the two-term branch.

Figure 3: Incremental growth of the certificate-study graph, rendered from the six saved graph files. Each small map contains all records and inference segments in that version; positions follow proof depth, and scopes, targets, computations, and claims retain different colors. After v001, heavier outlines mark newly added records. Counts measure records, not independent theorems. The compact maps show structure; the companion opens each version at full resolution with statements and evidence.

Panel of Figure 4 — Figure 4: Proof outline of the exact theorem, with the original-parameter scope attached throughout. Blue boxes denote inherited or classical inputs; green boxes show the certificate transfer and resulting bounds. The two upper routes are conditional arguments combined by exhaustive cases; for $n=2$ , only Case A occurs. The lower functional and either applicable upper route yield equality. Each box summarizes the indicated lemma or argument in appendix A ; the companion expands its recorded premises.

Figure 5: The implemented companion connects a selected graph record to its statement, scope, and hash-pinned evidence. The view focuses on the balanced transfer used to extend the boundary certificate. It is an interface excerpt; the versioned companion provides the full graph and prerequisite traces.

Claim to evaluate	Evidence available here	Further evidence needed
Recorded recursive investigation is feasible	One run with successive generated targets and six graph revisions	Multiple independently executed runs
Mathematical outcomes are correct	Full theorem proofs, an explicit certificate, and exact replay	Independent mathematical review; selected formalization
Graphs improve discovery	No controlled comparison	Matched baselines and preregistered milestones
Records support cumulative reuse	Reuse within the selected run	Later users and held-out objectives
Replay reduces review effort	Saved artifacts and internal replay	Independent reconstruction and cost measurement
Exploration paths support learning	Proposed exercises and interfaces	Student studies with transfer outcomes

Table 8: Current evidence and the evaluations required for stronger claims.

Appendix figures & tables8 assets

Supplementary material from the paper’s appendix.

Appendix

$\kappa$	$p$	$q$	$(\alpha,i,j)$
$-1$	$1$	$1$	$(1,0,1)$
$4$	$1$	$a_{1}b_{1}c_{1}$	$(0,0,1)$
$-2$	$1$	$a_{1}b_{0}c_{1}$	$(0,1,1)$
$2$	$1$	$a_{0}a_{1}b_{0}b_{1}c_{1}^{2}$	$(1,0,1)$
$-2$	$1$	$a_{0}a_{1}b_{0}^{2}c_{1}^{2}$	$(0,1,0)$
$2$	$1$	$a_{0}a_{1}b_{0}^{2}c_{1}^{2}$	$(1,0,0)$

Appendix

Table 9: The complete boundary certificate. Each row contributes

\kappa A(p,q)F_{\alpha ij}

; their sum is the constant one.

Derived expression	Maximum original product degree
Entries of $L,R^{\prime}$	$m+2$
$S_{r},T_{r},W_{r}$	$2m+3$
$V_{r}$	$m+3$
$K_{r}=Ud_{r}$	$2m+4$
$Z=U$	$2m+6$
$PZ=\det X$	$3m+6$

Appendix

Table 10: Degree ledger for the nilpotent-pencil certificate. Derived equations are charged through their representations in the original cubic generators.

Record	Core fields	Semantic requirement
Claim	ID, revision, statement, role, scope, source	Quantifiers and parameter regime belong to the statement; reconstructed text and source evidence remain distinguishable.
Inference	ID, premise IDs, conclusion, scope, justification	All premises are jointly required. Alternative proofs and conditional branches receive separate records.
Target	ID, parent, statement, objective link, bounds, status	Success must meet the stated quantitative requirement; partial results remain separately usable.
Objective	ID, origin, rationale, acceptance conditions, revision	Preserve the original objective and any prospectively recorded family changes.
Evidence	Type, location, hash, inputs, environment	Distinguish exact computations, source assertions, written proofs, and formal certificates.
Review	Reviewer role, coverage, method, findings	Report the actual scope of checking.

Appendix

Table 16

Artifact	What it makes reproducible or inspectable
Charter and initial source pins	Prospective objective, degree convention, inherited inputs
Six graphs and version deltas	Incremental additions, revisions, and retained open questions
Event history and replay index	Targets, actions, outcomes, actor attribution, and artifact versions
Mathematical notes and certificate table	Uniform arguments and the complete degree-9 identity
Rational certificates for three single-block pencils	Raw-variable unit identities of degrees 9, 12, and 15
Transfer and contraction checks	All-order construction tested on explicit finite inputs

Appendix

Table 12: Principal artifacts of the certificate-degree case study. Exact filenames and replay commands are supplied in the companion documentation.

Recorded events	Effect on the investigation and graph
E0001–E0004	Adopt the objective and initial targets, seal v001, and publish its atlas component.
E0005–E0008	Perform the first degree tests, verify the matrix-pencil baseline, extend the lower functional to unequal dimensions, and prove complete symmetry reduction.
E0009–E0012	Generate the all-size sharp-bound and target-grading questions, publish v002, and replay the rational certificates by raw expansion.
E0013–E0015	Use target grading, begin the rational lift of the degree-15 test, and save its exact certificate and expansion.
E0016–E0019	Generate the uniform commutator target, check its identities, record the all- $m$ theorem, and generate the remaining endpoint question.
E0020–E0021	Seal and publish v003 with the uniform theorem and its proof obligations.

Appendix

Table 18

Dated atlas state	Nodes	AND inferences
October 25: original extraction	58,916	19,516
October 31: before the case study	63,494	22,183
October 31: after the case study	63,562	22,217

Appendix

Table 14: Cumulative atlas counts through October 31, 2026. Each row is a complete dated state, not an additional component. Only the registered version of each component is counted, and references to existing base nodes are not counted again.

Unit	Count	Interpretation
Primary documents	1,874	Source files or sections, not necessarily papers
Reconciled history documents	855	Earlier records related to later argument records
Extraction batches	4,200	Units of annotation and accounting
Mathematical argument groups	7,738	Local groups of claims, scopes, and steps
History and support groups	17,406	Documentary, review, and supporting records
Nodes	58,916	Multiple semantic roles, not only theorems

Appendix

Table 15: The complexity atlas snapshot completed on October 25, 2026. Counts are different units and should not be added as if they measured independent results.

Record	Implemented information
Source	Path, full-file SHA-256, snapshot path, source role
Evidence anchor	Source ID, inclusive line interval, exact decoded passage, passage SHA-256
Node	Stable ID, authored title, verbatim source passages, role, source-reported status, scope IDs, review fields, planner eligibility
Inference	ID, premise IDs, conclusion, scope IDs, effective premises, reasoning mode, evidence; explicit assumption discharge where needed
Argument group	Nodes, targets, inferences, scope, and interpretation of conditional hypotheses
Navigation relation	Endpoints, relationship kind, explanatory note, and asserts_entailment=false

Appendix

Table 16: Existing atlas records. An authored summary and its verbatim evidence remain separate.

Mathematical Reasoning

Mathematical reasoning studies how AI systems solve problems, construct proofs, use tools, and discover or verify mathematical results.

See all 157 papers

May 9, 2026

Re $^2$ Math: Benchmarking Theorem Retrieval in Research-Level Mathematics

Large language models are increasingly capable at closed-world mathematical reasoning, but research assistance also requires source-grounded use of the literature. When a proof reaches a non-trivial step, a useful assistant should determine whether the needed tool (e.g., a lemma) already exists, identify a suitable scholarly source, and verify that its assumptions align with the current proof context. To rigorously evaluate such capabilities, we introduce Re

^2

Math, a benchmark for tool-grounded retrieval from partial mathematical proofs. Each instance is built from a candidate instrumental citation in the proof of a main theorem, with hierarchical context and an optional leakage-controlled anchor hint. We also make the task source-grounded yet citation-agnostic in that any admissible theorem sufficient for the proof transition is accepted. Evaluation uses a release-frozen retrieval artifact, ensuring reproducibility, while the benchmark itself supports automatic, continual expansion with newly constructed instances. On the current benchmark test set, the best fixed-judge ToolAcc reaches 7.0%, despite substantially higher rates of source grounding, indicating that current systems often retrieve valid statements but fail to establish their applicability to the local proof step. By decoupling citation recall, grounding, and proof-gap sufficiency, Re

^2

Math transforms literature-grounded mathematical tool use into a controlled diagnostic task.

Zicheng Lyu, Wenjie Yang, Shengzhong Zhang +1

Fudan University Shanghai, China · Nanjing University of Aeronautics and Astronautics Nanjing, Jiangsu, China · Fudan University Shanghai Innovation Institute Shanghai, China

Mathematical Reasoning Benchmarks LLM Evaluation Mathematical Reasoning Information Retrieval Evidence Retrieval

Ask PDF

May 20, 2026

RMA: Context-Orchestrated Research Math Agents

Long-horizon mathematical reasoning fails less often because a model cannot produce a valid next step than because an agent fails to maintain and expose the right semantic state across many iterations. Left unmanaged, this produces research-level proofs that are locally convincing yet globally incomplete: a key lemma unproved, an assumption unchecked, a citation unsupported, or a computational claim unverified. We present Research Math Agents (RMA), an agentic framework for long-horizon proof development built around a persistent, typed research store and an orchestrator that compiles operation-specific context from that store. The Research Context Orchestrator is the central state-management layer between the persistent research store and each locally scoped proof operation: it retrieves task-relevant artifacts, compiles them into a bounded context, invokes the appropriate operation, and writes the resulting proof edits, issue updates, literature notes, plans, or evaluations back to the store. This process is designed to keep proof revisions, unresolved issues, prior attempts, literature, and evaluations available across rounds while exposing only task-relevant state to each local operation. We evaluate RMA across complementary research-level settings using independent expert evaluation, blind mathematician review, LLM-based benchmark evaluation, and Lean 4 kernel verification. RMA achieves a 42.5% solve rate on the independently evaluated SOOHAK Challenge Hard set, obtains 8 of 10 correct solutions on First Proof B1 and 8 of 10 passing solutions on B2 under human-expert evaluation, and verifies 213 of 300 sampled Research Solved targets in Formal Conjectures with the Lean 4 kernel.

Zelin Zhao, Bo Yuan, Yuchen Zhu +2

Georgia Institute of Technology

LLM Context Management LLM Mathematical Reasoning Autonomous Research Agents Memory-Augmented Language Model Agents

Ask PDF

Oct 2, 2026

Continual Graph Memory and Community Infrastructure for AI-Assisted Mathematical Discovery

Mathematical discovery requires preserving partial ideas and the evidence supporting their reuse. We present Ansatz, a research harness whose continual graph memory separates model-accepted claims and dependencies from curated exploration, and Ansatze, a community platform for inspecting, guiding and checking this work. On First Proof, Ansatz recorded nine local verifier closures in each of two ten-problem batches; a partial result in the Second Batch also counted as a pass under the study's criterion. These model-assessed outcomes include continued searches and differ from expert validation. Component studies and re-review expose disagreements and their dependency reach. Open-problem investigations produced candidate results, with five Lean formalizations reported. The platform connects problem discovery, research records, manuscript analysis and formal checking while preserving distinct evidence states. Together, these systems support cumulative human-AI research through persistent investigation and inspectable contributions.

Eric Hanchen Jiang, Junyi Zhang, Jinxi Yu +27

University of California, Los Angeles

Autonomous Research Agents AI Agents for Scientific Discovery Graph-Based Agent Memory LLM Mathematical Reasoning

Ask PDF

Abstract

Mathematical Reasoning

Explore similar work

Re2^22Math: Benchmarking Theorem Retrieval in Research-Level Mathematics

RMA: Context-Orchestrated Research Math Agents

Continual Graph Memory and Community Infrastructure for AI-Assisted Mathematical Discovery

Re $^2$ Math: Benchmarking Theorem Retrieval in Research-Level Mathematics