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

Read PDF
Ask AI
Cite

Copy citation

DOINot available for this paper

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

OperationOne recorded stepDistinction to preserve
SUBA specified simultaneous substitutionDo not count one step per substituted symbol.
APPLYAn application of a theorem or identityFix the instance and its hypotheses; mere mention is insufficient.
EXPANDExpansion under a registered rulePrinted length is not the number of steps.
COLLECTCollection or cancellation in a fixed normal formDo not count the same normalization twice.
COMPONENTExtraction of a used component or coefficientA component is not the entire expression family.
CONSTRUCTConstruction of an object or mapRetain its defining conditions and source evidence.
Table 1: An illustrative operation registry. Each entry must be specialized by its allowed inputs, outputs, and context.
Figure 1: Equal bulk does not determine depth. The arrows record selected input use, and the displayed measurements concern the final state tt .
CaseSpecified inputRequired behavior
Shared prefixr→ar\to a , a→ba\to b , a→ca\to c , b→tb\to t , c→tc\to tD(t)=3D(t)=3 , S(t)=5S(t)=5 ; the prefix edge is counted once.
Alternative proofsRecords {a,b}⇒t\{a,b\}\Rightarrow t and {c}⇒t\{c\}\Rightarrow t ; select the second, with cc a sourceD(t)=1D(t)=1 , S(t)=1S(t)=1 ; do not add the first record’s inputs.
Internal uncertaintya→b→ta\to b\to t and U={b}U=\{b\}I(b)=I(t)=1I(b)=I(t)=1 , although bb is not a source.
Directed cyclea→b→aa\to b\to aReturn the cycle witness and block DAG metrics; do not delete an edge.
Anchor refinementReplace a→ba\to b by a→x→ba\to x\to b ; H={a,b}H=\{a,b\}Both skeletons contain a→ba\to b , while fine-grained depth and bulk change.
Table 2: Reference cases for PGPP 0.1. All edges point from input to output.
ObjectMain quantitiesRequired accompanying checks
Source inventoryPrecision and recall by item typeNumbered and unnumbered items assessed separately
Actual-use edgesPrecision, recall, and F1Supporting passages, contexts, and application hypotheses
DecompositionStep alignment and boundary agreementShared calculations and excessive subdivision
Macro skeletonAnchor ancestor-set agreementHeight, width, branching, and terminal structure
Depth and bulkAbsolute and relative error distributionsBoundary changes and unresolved components
ReproducibilityStructural and numerical agreementRecalculation distinguished from new extraction
Table 3: Proposed evaluation dimensions. No empirical values are asserted in this paper.
More in this topic

Mathematical Reasoning

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

See all 155 papers

Explore similar work

CardsList
May 9, 2026

Re2^2Math: 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 Re2^2Math, 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, Re2^2Math 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 BenchmarksLLM EvaluationMathematical ReasoningInformation RetrievalEvidence Retrieval
AskPDF
Jun 24, 2026

TheoremGraph: Bridging Formal and Informal Mathematics

Mathematical knowledge is organized around statements and their dependencies, but this structure is exposed unevenly: informal papers cite mostly at the document level, while formal libraries record fine-grained dependencies over a much smaller body of mathematics. We introduce TheoremGraph, a unified statement-level dependency graph spanning both informal and formal mathematics. On the informal side, we parse 11.7M theorem-like environments from mathematics arXiv and recover 18.3M candidate directed dependencies, each labeled by the extractor that proposed it so downstream users can trade coverage for precision. On the formal side, we release LeanGraph, a Lean 4 elaborator-level extractor producing 388,105 declaration nodes and 11.3M typed edges across 25 Lean projects. We bridge the two graphs by embedding generated natural-language slogans into a shared semantic space, linking related statements across papers and across the informal/formal divide; an LLM judge affirms 47,952 such matches above a 0.8 cosine floor, with the judge-acceptance rate rising from 48% across the floor to 87% in the >=0.9 tier. On formal concept retrieval, our name-and-signature representation with graph expansion comes within 0.5pp of LeanSearch v2's reranked Recall@10 (0.775 vs. 0.780) without an LM reranker. We release the dataset, extractors, HTTP API, and MCP interface as infrastructure for mathematical search, attribution, and retrieval-augmented reasoning, available at theoremsearch.com and huggingface.co/datasets/uw-math-ai/theorem-matching.

Simon Kurgan, Evan Wang, Eric Leonen +6

University of Washington Math AI Lab

KG ConstructionGraph-Based RetrievalKnowledge RepresentationInformation Retrieval
AskPDF
Jun 13, 2026

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

Large language models (LLMs) are increasingly capable of mathematical problem solving and can even assist with research-level proofs, yet we still lack a scalable and reproducible way to measure step-level reasoning in long proofs across diverse sources. This evaluation gap limits trustworthy AI assistance in proof-certified scientific progress. Existing evaluations often emphasize final answers or rely on costly expert grading, while end-to-end proof generation remains open-ended and hard to verify automatically. We introduce Mask-Proof, a pipeline that turns real proofs into automatically checkable masked-step tasks. It masks key formula steps, provides the necessary surrounding context, and evaluates model reconstructions with an LLM-based equivalence judge using repeated votes for stability. The resulting Mask-ProofBench contains 292 curated problems across diverse research areas. Experiments with 17 models show that reasoning-enhanced models outperform standard models by 12% to 27%. Our evaluator achieves 96.8% agreement with expert annotators, enabling faithful, reproducible, and comparable measurement of step-level mathematical reasoning. Benchmark, annotations, and code are available at https://github.com/weating/Mask-Proof.

Jierui Zhang, Siyuan Tan, Xinhang Li +8

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

Mathematical Reasoning BenchmarksLLM EvaluationAutomated Theorem ProvingTraining Data CurationLLM Mathematical Reasoning
AskPDF