Measuring and reviewing math proofs with dependency graphs
Dependency Graphs of Mathematical Arguments: Representation, Structural Measurement, and Proof Review
Artificial Intelligence
Summary
Mathematical proofs are complex and built from many smaller steps. This paper describes a way to represent and measure those steps using graphs that show how each statement depends on others. The authors use large language models to help manage the representation and review of proofs, keeping track of sources and versions. Their system can suggest missing parts and support reviewing both human-written and AI-generated proofs, though it does not yet prove these benefits with experiments.
What this means in practice
- •For software verification engineers: Use dependency graphs to visualize and check logical dependencies in formal verification proofs for complex software systems.
- •For document management teams: Implement version-controlled proof annotations to track changes and reviews in mathematical manuscripts supporting regulatory or patent documents.
A position paper. It proposes an approach and reports no results.
Authors
Eunji Park
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.