# Proof Repair across Type Equivalences

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

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 2 Oct 2020.

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

- [Can Transformers Learn to Solve Problems Recursively?](https://mlsanity.com/paper/2305.14699/) (2023)
- [Transformer-Based Models Are Not Yet Perfect At Learning to Emulate Structural Recursion](https://mlsanity.com/paper/2401.12947/) (2024)
- [LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction](https://mlsanity.com/paper/2502.17925/) (2025)
- [APE-Bench: Evaluating Automated Proof Engineering for Formal Math Libraries](https://mlsanity.com/paper/2504.19110/) (2025)
- [BlueprintRepair: Typed Local Edits for Failed Lean Proof Blueprints](https://mlsanity.com/paper/2607.28110/) (2026)
- [SelfHeal: Empirical Fix Pattern Analysis and Bug Repair in LLM Agents](https://mlsanity.com/paper/2604.17699/) (2026)
- [CAPRI: Contract-Aware Proof Repair for Isabelle](https://mlsanity.com/paper/2608.13459/) (2026)
- [Assurance Envelopes for Autonomous Coding Agents: Minimum-Cost Evidence for Software Change](https://mlsanity.com/paper/2609.16302/) (2026)

## Abstract (arXiv)

We describe a new approach to automatically repairing broken proofs in the Coq proof assistant in response to changes in types. Our approach combines a configurable proof term transformation with a decompiler from proof terms to tactic scripts. The proof term transformation implements transport across equivalences in a way that removes references to the old version of the changed type and does not rely on axioms beyond those Coq assumes. We have implemented this approach in PUMPKIN Pi, an extension to the PUMPKIN PATCH Coq plugin suite for proof repair. We demonstrate PUMPKIN Pi's flexibility on eight case studies, including supporting a benchmark from a user study, easing development with dependent types, porting functions and proofs between unary and binary numbers, and supporting an industrial proof engineer to interoperate between Coq and other verification tools more easily.