Improving math proofs for easier human understanding and memory
Optimising Metamath Proofs for Human Working Memory
Logic in Computer Science
Summary
Mathematical proofs can be hard to follow because of how they are ordered. Most techniques focus on making proofs shorter, but the authors show that changing the order of steps can make them easier for people to keep in mind without changing the length. They study this problem using Metamath, a system that usually orders proofs for computer speed rather than human readability. By treating proofs like puzzles on a graph and using strategies to reorder them, the authors find ways to reduce how much memory a person needs to understand the proof. Their method helps make formal math clearer and easier to work with.
Mathematical proofMetamathProof verificationWorking memoryDirected acyclic graphProof optimisationCognitive effortHeuristic algorithmsSet theoryPebbling game
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.