发表机构
University of Melbourne（墨尔本大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出通过将证明表示为有向无环图并建模为 pebbling 游戏，利用启发式算法最小化峰值和累积内存消耗，以优化 Metamath 证明的排序，提升形式化数学的可读性。
AI 中文摘要
数学证明的可读性各不相同。虽然大多数证明优化技术旨在最小化证明规模，但对推理步骤进行策略性重排序可以在不改变整体规模的情况下降低证明检查的工作记忆需求。Metamath 是这种方法的一个典型案例研究：其验证架构要求证明步骤的排序方式优先考虑算法效率而非可读性。在本文中，我们引入了最小化峰值和累积内存消耗的算法，并将后者作为持续人类认知努力的新颖代理指标。我们通过将证明表示为有向无环图并将其执行建模为一种 pebbling 游戏来实现这一目标。通过暴力搜索找到最优排序在计算上是不可行的，因此我们使用启发式方法提供近似解。我们将这些算法应用于 Metamath 的 ZFC 集合论库，并展示案例研究，证明自动重排序如何系统地改进形式化数学的呈现。
英文摘要
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.
CommentsSubmitted version. A revised version is to appear in CICM 2026, LNAI, Springer
