Optimising metamath proofs reduces human memory demand during checking
Optimising Metamath Proofs for Human Working Memory
Logic in Computer Science
Summary
Mathematical proofs can be hard to follow, especially when checking each step. The authors focus on Metamath, a system where proofs are arranged mainly for quick computer checking, not human understanding. They created methods to reorder proof steps to lower the mental effort needed to follow them, without changing the proof size. Their approach models proofs as graphs and uses clever heuristics to find better step orders, improving readability while keeping proofs valid.
What this means in practice
- •For formal verification engineers: Reduce mental effort needed to verify Metamath proofs by reordering steps to optimize human working memory.
- •For software developers: Improve readability of formal proofs used in software correctness tools by applying memory-aware proof step ordering.
Authors
Jeremy Lindsay, Cezary Kaliszyk, Christine Rizkallah
Abstract
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.