# What are the Right Symmetries for Formal Theorem Proving?

arXiv: https://arxiv.org/abs/2605.22257 · HTML: https://mlsanity.com/paper/2605.22257/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 43 of its 73 references that are in the map.
- First posted on arXiv 21 May 2026.

## Builds on (most cited first, 30 of 43)

- [Least-to-Most Prompting Enables Complex Reasoning in Large Language Models](https://mlsanity.com/paper/2205.10625/) (2022)
- [Geometric Deep Learning: Grids, Groups, Graphs, Geodesics, and Gauges](https://mlsanity.com/paper/2104.13478/) (2021)
- [Large Language Monkeys: Scaling Inference Compute with Repeated Sampling](https://mlsanity.com/paper/2407.21787/) (2024)
- [Counterfactual Fairness](https://mlsanity.com/paper/1703.06856/) (2017)
- [GSM-Symbolic: Understanding the Limitations of Mathematical Reasoning in Large Language Models](https://mlsanity.com/paper/2410.05229/) (2024)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [The Reversal Curse: LLMs trained on "A is B" fail to learn "B is A"](https://mlsanity.com/paper/2309.12288/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [On the Generalization of Equivariance and Convolution in Neural Networks to the Action of Compact Groups](https://mlsanity.com/paper/1802.03690/) (2018)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [Query Rewriting for Retrieval-Augmented Large Language Models](https://mlsanity.com/paper/2305.14283/) (2023)
- [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://mlsanity.com/paper/2408.08152/) (2024)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025)
- [Equivariance Through Parameter-Sharing](https://mlsanity.com/paper/1702.08389/) (2017)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [Equivariance with Learned Canonicalization Functions](https://mlsanity.com/paper/2211.06489/) (2022)
- [BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving](https://mlsanity.com/paper/2502.03438/) (2025)
- [On the Benefits of Invariance in Neural Networks](https://mlsanity.com/paper/2005.00178/) (2020)
- [Graph Representations for Higher-Order Logic and Theorem Proving](https://mlsanity.com/paper/1905.10006/) (2019)
- [Position: Categorical Deep Learning is an Algebraic Theory of All Architectures](https://mlsanity.com/paper/2402.15332/) (2024)
- [reWordBench: Benchmarking and Improving the Robustness of Reward Models with Transformed Inputs](https://mlsanity.com/paper/2503.11751/) (2025)
- [Lie Algebra Canonicalization: Equivariant Neural Operators under arbitrary Lie Groups](https://mlsanity.com/paper/2410.02698/) (2024)
- [EquiBench: Benchmarking Large Language Models' Reasoning about Program Semantics via Equivalence Checking](https://mlsanity.com/paper/2502.12466/) (2025)
- [ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization](https://mlsanity.com/paper/2510.15981/) (2025)
- [Consistency Training Helps Stop Sycophancy and Jailbreaks](https://mlsanity.com/paper/2510.27062/) (2025)
- [Graph2Tac: Online Representation Learning of Formal Math Concepts](https://mlsanity.com/paper/2401.02949/) (2024)
- [Revisiting Random Walks for Learning on Graphs](https://mlsanity.com/paper/2407.01214/) (2024)

## Built on by (most cited first, 1 of 1)

- [EULER: Exploring Underused Links with Evidence-Checked Return for Multi-Agent Mathematical Discovery](https://mlsanity.com/paper/2609.00032/) (2026)

## Abstract (arXiv)

Formal theorem provers based on large language models (LLMs) are highly sensitive to superficial variations in problem representation: semantically equivalent statements can exhibit drastically different proof success rates, revealing a failure to respect structural symmetries inherent in formal mathematics. This raises a central question: what are the right symmetries for formal theorem proving? We introduce rewriting categories, a category-theoretic framework capturing the compositional, generally non-invertible transformations induced by proof tactics, and use it to formalize two symmetry notions: proof equivariance, governing how proof distributions transform under rewrites, and success invariance (i.e., invariance of success probability), requiring equivalent statements to be solved with the same probability. We observe that state-based next-tactic provers naturally satisfy proof equivariance by operating on proof states. In contrast, state-of-the-art LLM-based provers satisfy neither property, exhibiting large performance variation across equivalent formulations. To mitigate this, we propose test-time methods that aggregate over equivalent rewritings of the input, showing theoretically that they recover success invariance in the sampling limit, and empirically, that they improve robustness and performance under fixed inference budgets. Our results highlight symmetry as a key missing inductive bias in LLM-based theorem proving and suggest test-time computation as a practical route to approximate it.