Source-linked AI summary
Optimising Metamath Proofs for Human Working Memory
Jeremy Lindsay, Cezary Kaliszyk, Christine Rizkallah
TL;DR
Proof readability depends partly on working-memory demand, while Metamath’s native ordering is designed for verification rather than readability. The paper models proof orderings with DAGs and pebbling games, then uses heuristics to reorder steps. Its heuristics improve peak and cumulative memory use on many set.mm proofs while preserving proof length.
Problem
Method
The paper represents proofs as DAGs, models memory use with pebbling games, and uses heuristic algorithms to reorder proof steps.
Source: §1 · p. 2Results
Heuristic DFS algorithms improve peak and cumulative memory consumption on many set.mm proofs while preserving proof length.
Source: §10 · p. 15Takeaways & Limitations
The results support proof reordering as a practical optimization target for legibility proxy metrics and motivate evaluation on formal libraries beyond Metamath.
Source: §10 · p. 15Pebbling games use live mathematical expressions only as a proxy for working-memory load, and readability may not noticeably improve when optimal space or cumulative cost is very high.
Source: §5 · p. 7
Abstract
from arXiv · showhide
Mathematical proofs vary in legibility. While most proof optimisation techniques seek to minimise proof size, the strategic reordering of inferences can reduce the working memory demand of proof checking without altering overall size. Metamath serves as a prime case study for this approach: its verification architecture requires proof steps to be ordered in a manner that prioritises algorithmic efficiency over readability. In this paper, we introduce algorithms to minimise both peak and cumulative memory consumption, applying the latter as a novel proxy for sustained human cognitive effort. We achieve this by representing proofs as directed acyclic graphs and modelling their execution as a pebbling game. Finding an optimal ordering via brute force is computationally infeasible, so we use heuristics to provide approximations. We apply these algorithms across Metamath's ZFC set theory library and present case studies demonstrating how automated reordering systematically improves the presentation of formal mathematics.
1 Introduction
Proof readability depends partly on the working-memory demand of following a proof, so this paper reorders proof steps to reduce memory use without changing proof length. It models proofs as dependency graphs and uses heuristic algorithms to study this approach in Metamath’s ZFC library.
1 Introduction
- The algorithms target both peak memory use and cumulative memory use while preserving proof length.Cumulative memory use captures sustained demand across the proof, alongside the better-studied peak-memory objective.Source: §1 · pp. 1–2
- Metamath is a testbed because its proofs have explicit dependencies but native step ordering prioritizes verification over readability.The methods are described as general-purpose and require only abstract graph-based proof representations.Source: §1 · p. 2
- Proofs are represented as directed acyclic graphs, with sequential presentations corresponding to topological orders, and memory demand modeled through pebbling games.Because brute-force optimal ordering is infeasible in practice, the paper uses heuristics.Source: §1 · p. 2
- The paper introduces metrics inspired by Karol Pąk’s legibility metrics and compares them with memory-consumption measures.The supplied introduction identifies mean index distance and adjacency rate as related metrics.Source: §1 · p. 2
- The paper introduces a pebbling variant that makes unpebbling automatic, simplifying memory calculations.It also develops heuristic reordering methods combining ideas from Fellner and Paleo.Source: §1 · p. 2
- The algorithms are applied to Metamath’s ZFC library set.mm, with analyses and case studies.The introduction names Paleo’s greedy algorithm [5], Sethi–Ullman numbering, and other lightweight ordering criteria.Source: §1 · p. 2
- The work frames proof legibility as a concern that may grow as LLM-based proof generation and transformation become more common [25].Source: §1 · p. 2
2 Related Work
This work shifts proof optimization from shortening proofs to examining how step order affects memory use and legibility while proof length stays constant. It relates that focus to prior legibility metrics and pebbling-based space optimization.
2 Related Work
- The paper studies how proof-step ordering affects memory consumption and legibility while holding overall proof length constant.This contrasts with common optimization targets such as proof length or verification time.Source: §2 · pp. 2–3
- Pąk’s legibility metrics use the close reference principle, whereas this work models memory consumption as it evolves during proof checking.The paper also introduces mean index distance and adjacency rate inspired by Pąk’s methods and, respectively.Source: §2 · p. 3
- Fellner and Paleo studied peak-memory optimization for machine-generated resolution proofs; this work also treats cumulative memory as a proxy for sustained human cognitive load.Its depth-first search approach is inspired by their greedy algorithm.Source: §2 · p. 3
3 Metamath
Metamath is a logic-agnostic proof assistant whose mathematical content depends on user-specified axioms; this paper focuses on its ZFC library set.mm. Its stack-based verification order can make proofs difficult to read when expressions remain unreferenced for many steps.
3 Metamath
- Metamath contains no inherent mathematical content without axioms, and this paper focuses on the ZFC set theory library set.mm.The paper describes set.mm as Metamath’s largest and most mature library.Source: §3 · p. 3
- Verification uses a stack: proof steps introduce assumptions or apply inference rules, and theorem applications consume ordered premises to produce a conclusion.The mp2 example applies modus ponens twice to derive its goal formula.Source: §3 · pp. 3–4
- Table 1 tracks the mp2 stack across proof steps, with columns for steps and rows for stack positions.Source: Table 1 · p. 4
- Metamath’s precise evaluation order can leave an expression unreferenced until much later, making native proofs laborious to read.In the cited prmunb example, the first step is not referenced until 47 steps later.Source: §3 · p. 4
4 Proof DAGs and Topological Orders
Proofs are represented as DAGs of distinct inferences, with edges encoding direct dependencies and premise positions. Valid presentations are topological orders, evaluated in part by how close dependent steps appear.
4 Proof DAGs and Topological Orders
- A proof DAG is an acyclic graph with a unique sink; its vertices are distinct inferences, and each edge records a direct dependency and the premise index used.The vertex-to-expression map need not be injective, so an expression may be derived more than once.Source: §4 · p. 5
- Each valid linearisation is a topological order, and mean index distance averages the separation between dependency-linked inferences.The index distance between two vertices is the absolute difference between their positions in the order.Source: §4 · p. 5
- Legibility is ideally maximised when every dependency edge connects consecutive inferences; adjacency rate measures how often this occurs.Source: §4 · p. 6
5 Pebbling Games
Pebbling models the expressions that must remain available while a proof is checked, allowing memory demand to be assessed across a sequence of inferences. The paper restricts pebbling to reflect a fixed proof order and distinguishes peak space from cumulative cost.
5 Pebbling Games
- Pebbling treats a stored expression as a pebble on its inference, and a proof strategy proceeds from an empty configuration to the conclusion’s sink.Each legal move pebbles a source or a vertex whose predecessors are pebbled, or unpebbles a vertex.Source: §5 · p. 6
- The one-shot, implicit-unpebbling variant permits each inference to be evaluated once and automatically releases it after all its successors have been pebbled.This fixes memory usage according to which expressions still have future uses, rather than leaving release timing to the player.Source: §5 · pp. 6–7
- Pebbling metrics treat live mathematical expressions only as a proxy for audience working-memory load, not the presenter’s explicit memory management.The authors also caution that readability may not noticeably improve when optimal space or cumulative cost is very high.Source: §5 · p. 7
- Space and cumulative cost can favour different strategies: Table 2 shows space 3 versus 2, while Table 3 shows equal space 2 but cumulative costs 6 versus 5.The different outcomes illustrate that minimising peak space need not minimise cost accumulated over the sequence.Source: §5 · p. 7, Table 2 · p. 8, Table 3 · p. 8
- A topological order induces a canonical pebbling strategy by adding each ordered vertex and then applying implicit unpebbling.Source: §5 · p. 8
6 Proof Reordering Algorithms
The algorithms search for a proof-DAG traversal that minimizes pebbling space and cumulative cost by ordering each inference’s predecessors according to lightweight policies. Recursive branch-weight heuristics prioritize heavier branches, with the original order resolving ties.
6 Proof Reordering Algorithms
- A bottom-up depth-first search orders a proof DAG by recursively visiting each vertex’s predecessors according to a selected policy, then appending the vertex.The goal is a pebbling strategy with minimized space and cumulative cost.Source: §6 · p. 8
- Ordering policies rank predecessors using the original premise order, random choice, Sethi-Ullman weights, cumulative-cost weights, successor counts, or last-successor weights.The policies define predecessor orders at each vertex; strict orders can be formed by appending Original as a tie-breaker.Source: §6 · pp. 8–9
- The policies use recursive weights for Sethi-Ullman, cumulative-SU, and cumulative-predecessor measures, while LastSucc counts edges that are last among a vertex’s successors.Source weights are zero for LastSucc and one for the other policies.Source: §6 · p. 9
- CumulSU and CumulPred adapt predecessor weights to target cumulative cost, while LastSucc comes from Fellner and Paleo’s best-performing heuristic.The paper’s rationale is to evaluate heavier branches earlier so intermediate results need to remain in memory for less time.Source: §6 · p. 9
7 Experiments
The experiments apply DFS-based ordering policies to proof DAGs from set.mm and compare their pebbling metrics across treelike and non-treelike proofs. Mixed SU and cumulative-cost policies are reported as the strongest overall approach for jointly optimizing space and cumulative cost.
7.1 Methodology
- The study converts set.mm proofs into DAGs from verifier stack-operation logs, then runs Algorithm 1 under four specified policy combinations.The combinations are (SU, Original), (SU, CumulSU, Original), (CumulPred, Original), and (NumSucc, Original).Source: §7 · p. 9, §7.1 · p. 11
7 Experiments
- The original set.mm proofs have heavily right-skewed distributions, with median statement count 15, median pebbling space 5, and median cumulative cost 38.Figure 3 presents these box plots on a log scale.Source: Figure 3 · p. 10
7.1 Methodology
- The evaluation measures relative changes in space and cumulative cost, regressions, attainment of the space lower bound, and execution time.Execution times are ranked across set.mm in Table 7.Source: §7.1 · p. 11, §7.2 · p. 13, Table 7 · p. 13
- Across 47,248 proofs, 29,338 are treelike, so results distinguish trees from non-treelike proofs.Sethi-Ullman numbering and its generalization are optimal for pebbling space on trees.Source: §7.1 · p. 11
7.2 Results
- CumulPred and CumulSU perform similarly on cumulative cost, and combining SU with either policy appears best overall for optimizing both space and cumulative cost.Table 4 compares average metrics against the original Metamath ordering, separately for treelike and non-treelike proofs.Source: §7.2 · pp. 11–12, Table 4 · p. 12
- Table 5 reports how often each policy performs worse than Original, with results separated for treelike and non-treelike proofs.SU is optimal for treelike proofs; a non-treelike example illustrates an inherent limitation of DFS.Source: Table 5 · p. 12, §7.2 · p. 12
- For treelike proofs, the lower-bound space rate improves over Original by more than 30%; for non-treelike proofs, the best policies attain it almost six times as often as Original.SU is optimal with respect to space on trees.Source: §7.2 · p. 13, Table 6 · p. 13
8 Case Studies
The case studies show that reordering can reduce proof-memory demands by delaying premises until nearer their use, while memory objectives may trade off and DFS can produce worse orderings in some cases.
8 Case Studies
- Space falls from 9 to 6 and cumulative cost from 224 to 137 when the policy delays nnnn0 until step 47.The original proof introduces nnnn0 at the first step although it is not used until step 48.Source: §8 · p. 14
- Pebbling space drops from 4 to the lower bound of 2, and cumulative cost from 20 to 12, when inferences A and B are scheduled just before they are needed.The reordered proof makes the A–H and B–G dependency edges have unit index distance.Source: §8 · p. 14
- MID rises from 2.6 to 2.7, while space falls from 5 to 4 and cumulative cost from 24 to 21, showing a trade-off between memory measures and index distance.The reordered proof has three edges with unit index distance, versus four in the original.Source: §8 · p. 14
- Table 3 shows cumulative cost can improve with unchanged space, while Figure 4(c) illustrates an example where space worsens.The supplied passages do not give the Figure 4(c) metric values.Source: §8 · pp. 14–15
- Cumulative cost falls from 31 to 27 even as space rises from 3 to 4, because the reordered traversal holds ε(N) for fewer steps than ε(E).The new ordering creates the bottleneck configuration {N, B, C, D}.Source: §8 · p. 15
- In 4.31% of cases, the policy produces a worse ordering, with space rising from 3 to 4 and cumulative cost from 20 to 21; DFS cannot interleave predecessors of different vertices out of order.The bottleneck configuration for space is {C, G, D, E}.Source: §8 · p. 15
9 Future Work
Future work could extend the proof-DAG methods to backward reasoning and other mathematical libraries, and could model differences in expression complexity with weighted pebbling.
9 Future Work
- Backward reasoning in proof DAGs could be explored using black-white pebbling games.The passage presents this as a possible way to adapt the methods.Source: §9 · p. 15
- The methods may be adapted for Mizar, Lean’s Mathlib, and Isabelle/HOL’s AFP.The proposed extension is to other mathematical libraries beyond the current Metamath setting.Source: §9 · p. 15
- Weighted pebbling games could assign higher weights to expressions with more symbols or deeper nested structure.This would capture variations in mathematical-expression complexity.Source: §9 · p. 15
10 Conclusion
The paper studies proof-step reordering in Metamath with pebbling games and reports memory improvements on many set.mm proofs without changing their length. Its case studies also identify failures, while motivating proof reordering as a legibility-optimization target and further evaluation beyond Metamath.
10 Conclusion
- Heuristic DFS algorithms improve peak and cumulative memory consumption on many set.mm proofs while preserving proof length.The paper uses pebbling games to study how reordering Metamath proof steps affects verification memory.Source: §10 · p. 15
- Case studies illustrate how improvements arise and where they may fail, including an inherent limitation of DFS.The conclusion does not claim every proof benefits from reordering.Source: §10 · p. 15
- The results support proof reordering as a practical target for legibility proxy metrics and motivate evaluation on formal libraries beyond Metamath.Source: §10 · p. 15