Dependency Graphs of Mathematical Arguments: Representation, Structural Measurement, and Proof Review

Eunji Park

cs.AIOct 27, 2026

Dependency Graphs of Mathematical Arguments: Representation, Structural Measurement, and Proof Review

Authors: Eunji Park

Organizations: Graduate School of Data Science, Seoul National University, Gwanak-ro 1, Gwanak-gu, Seoul 08826, Korea

Abstract

We propose a source-grounded framework for representing and measuring mathematical arguments with assistance from large language models. It includes numbered and unnumbered statements, equations, assumptions, and constructions, distinguishing source occurrences from contextual states and inference records. Proposed dependencies retain source evidence and review status. A measurement contract fixes manuscript versions, boundaries, granularity, proof choices, and macro anchors. On a selected finite directed acyclic graph, depth is the longest prerequisite-path length, and bulk counts distinct ancestor edges. We give a union recurrence that accounts for shared subarguments and identify reachability conditions preserving depth and the macro skeleton; unrestricted refinement need not preserve depth or bulk. A standardized, versioned prompt protocol separates annotation discovery, deterministic recomputation, and review assistance. Cross-paper links support a research agenda on theorem co-use, rare combinations, and connections between dependency communities. These patterns motivate probabilistic premise suggestions and review of possible omissions or unchecked application conditions in human-written and AI-generated proofs. Further applications include source-linked reading support and comparison of individual and collaborative argument shapes. We provide an evaluation design rather than empirical evidence of these benefits. Suggested premises require mathematical validation, and the measures describe a specified representation rather than intrinsic mathematical difficulty, originality, or importance.

Figures & tables

Operation	One recorded step	Distinction to preserve
SUB	A specified simultaneous substitution	Do not count one step per substituted symbol.
APPLY	An application of a theorem or identity	Fix the instance and its hypotheses; mere mention is insufficient.
EXPAND	Expansion under a registered rule	Printed length is not the number of steps.
COLLECT	Collection or cancellation in a fixed normal form	Do not count the same normalization twice.
COMPONENT	Extraction of a used component or coefficient	A component is not the entire expression family.
CONSTRUCT	Construction of an object or map	Retain its defining conditions and source evidence.

Table 1: An illustrative operation registry. Each entry must be specialized by its allowed inputs, outputs, and context.

Panel of Figure 1 — Figure 1: Equal bulk does not determine depth. The arrows record selected input use, and the displayed measurements concern the final state $t$ .

Case	Specified input	Required behavior
Shared prefix	$r\to a$ , $a\to b$ , $a\to c$ , $b\to t$ , $c\to t$	$D(t)=3$ , $S(t)=5$ ; the prefix edge is counted once.
Alternative proofs	Records $\{a,b\}\Rightarrow t$ and $\{c\}\Rightarrow t$ ; select the second, with $c$ a source	$D(t)=1$ , $S(t)=1$ ; do not add the first record’s inputs.
Internal uncertainty	$a\to b\to t$ and $U=\{b\}$	$I(b)=I(t)=1$ , although $b$ is not a source.
Directed cycle	$a\to b\to a$	Return the cycle witness and block DAG metrics; do not delete an edge.
Anchor refinement	Replace $a\to b$ by $a\to x\to b$ ; $H=\{a,b\}$	Both skeletons contain $a\to b$ , while fine-grained depth and bulk change.

Table 2: Reference cases for PGPP 0.1. All edges point from input to output.

Object	Main quantities	Required accompanying checks
Source inventory	Precision and recall by item type	Numbered and unnumbered items assessed separately
Actual-use edges	Precision, recall, and F1	Supporting passages, contexts, and application hypotheses
Decomposition	Step alignment and boundary agreement	Shared calculations and excessive subdivision
Macro skeleton	Anchor ancestor-set agreement	Height, width, branching, and terminal structure
Depth and bulk	Absolute and relative error distributions	Boundary changes and unresolved components
Reproducibility	Structural and numerical agreement	Recalculation distinguished from new extraction

Table 3: Proposed evaluation dimensions. No empirical values are asserted in this paper.

Mathematical Reasoning

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

See all 155 papers

Re $^2$ Math: Benchmarking Theorem Retrieval in Research-Level Mathematics
May 9, 2026Zicheng Lyu, Wenjie Yang, Shengzhong Zhang +1Mathematical Reasoning Benchmarks LLM Evaluation
Fudan University Shanghai, China · Nanjing University of Aeronautics and Astronautics Nanjing, Jiangsu, China · Fudan University Shanghai Innovation Institute Shanghai, China
TheoremGraph: Bridging Formal and Informal Mathematics
Jun 24, 2026Simon Kurgan, Evan Wang, Eric Leonen +6KG Construction Graph-Based Retrieval
University of Washington Math AI Lab
Mask-Proof: An LLM-based Automated Data Curation Pipeline on Mathematical Proofs
Jun 13, 2026Jierui Zhang, Siyuan Tan, Xinhang Li +8Mathematical Reasoning Benchmarks LLM Evaluation
School of Computer Science Beijing University of Posts and Telecommunications Beijing, China · Graduate College for Engineers Beijing University of Posts and Telecommunications Beijing, China · School of Mathematical Sciences Fudan University Shanghai, China +6

May 9, 2026J/K move · Enter open · S save

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

Zicheng Lyu, Wenjie Yang, Shengzhong Zhang, Zengfeng Huang

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

Open paper AskPDF arXiv

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.

Abstract

Mathematical Reasoning

Explore similar work

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

TheoremGraph: Bridging Formal and Informal Mathematics

Mask-Proof: An LLM-based Automated Data Curation Pipeline on Mathematical Proofs

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