New preprint: What are the Right Symmetries for Formal Theorem Proving?

LLM-based theorem provers can succeed or fail on statements that are mathematically equivalent. In What are the Right Symmetries for Formal Theorem Proving?, led by Krzysztof Olejniczak, we introduce rewriting categories to formalise which symmetries provers should respect, such as proof equivariance and success invariance.