Document Open Access Logo

Automatically Generalizing Proofs and Statements

Authors Anshula Gandhi , Anand Rao Tadipatri , Timothy Gowers

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2025.12.pdf
  • Filesize: 0.77 MB
  • 18 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Automated reasoning
Keywords
  • automated reasoning
  • automated theorem proving
  • interactive theorem proving
  • formalization of mathematics
  • generalization
  • Lean theorem prover
  • Lean tactic

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

We present an algorithm, developed in the Lean programming language, to automatically generalize mathematical proofs. The algorithm, which builds on work by Olivier Pons, advances state-of-the-art proof generalization by robustly generalizing repeated and related constants, as well as abstracting out hypotheses implicitly concerning them. We also discuss the role of proof generalization in conjecturing, learning from failure, and other aspects of mathematical proof discovery.

Cite As Get BibTex

Anshula Gandhi, Anand Rao Tadipatri, and Timothy Gowers. Automatically Generalizing Proofs and Statements. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 12:1-12:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ITP.2025.12

Author Details

Anshula Gandhi
  • University of Cambridge, UK
Anand Rao Tadipatri
  • University of Cambridge, UK
Timothy Gowers
  • Collège de France, Paris, France
  • University of Cambridge, UK

Supplementary Materials

References

  1. Alexander Best. Automatically generalizing theorems using typeclasses. In Conference on Intelligent Computer Mathematics, 2021. URL: https://ceur-ws.org/Vol-3377/fmm12.pdf.
  2. Thierry Boy De La Tour and Nicolas Peltier. Proof generalization in LK by second order unifier minimization. Journal of Automated Reasoning, 57(3):245-280, 2016. Google Scholar
  3. Robert Boyer and J. Strother Moore. A Computational Logic, chapter 12: Generalization, pages 163-170. Academic Press, 1979. Google Scholar
  4. Amy Felty and Douglas Howe. Generalization and reuse of tactic proofs. In Logic Programming and Automated Reasoning: 5th International Conference, LPAR'94 Kiev, Ukraine, July 16-22, 1994 Proceedings 5, pages 1-15. Springer, 1994. URL: https://doi.org/10.1007/3-540-58216-9_25.
  5. Robert W Hasker and Uday S Reddy. Generalization at higher types. In Proceedings of the Workshop on the λProlog Programming Language, pages 257-271, 1992. Google Scholar
  6. Andrew Ireland and Alan Bundy. Productive use of failure in inductive proof. Journal of Automated Reasoning, 16(1-2):79-111, 1996. URL: https://doi.org/10.1007/BF00244460.
  7. Einar Broch Johnsen and Christoph Lüth. Theorem reuse by proof term transformation. In International Conference on Theorem Proving in Higher Order Logics, pages 152-167. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-30142-4_12.
  8. Thomas Kolbe and Christoph Walther. Proof analysis, generalization and reuse. In Automated Deduction—A Basis for Applications: Volume II: Systems and Implementation Techniques, pages 189-219. Springer, 1998. Google Scholar
  9. Nicolas Magaud and Yves Bertot. Changing data structures in type theory: A study of natural numbers. In International Workshop on Types for Proofs and Programs, pages 181-196. Springer, 2000. URL: https://doi.org/10.1007/3-540-45842-5_12.
  10. Brigitte Pientka. Mechanizing meta-theory in beluga (invited talk). In Yuki Chiba, Santiago Escobar, Naoki Nishida, David Sabel, and Manfred Schmidt-Schauß, editors, 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE@RDP 2015, July 2, 2015, Warsaw, Poland, volume 46 of OASIcs, pages 1-1. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. URL: https://doi.org/10.4230/OASICS.WPTE.2015.1.
  11. Gordon D Plotkin. A note on inductive generalization. Machine intelligence, 5(1):153-163, 1970. Google Scholar
  12. Olivier Pons. Generalization in type theory based proof assistants. In Paul Callaghan, Zhaohui Luo, James McKinna, and Robert Pollack, editors, Types for Proofs and Programs, International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000, Selected Papers, volume 2277 of Lecture Notes in Computer Science, pages 217-232. Springer, 2000. URL: https://doi.org/10.1007/3-540-45842-5_14.
  13. Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, Zachary Tatlock, et al. QED at large: A survey of engineering of formally verified software. Foundations and Trends® in Programming Languages, 5(2-3):102-281, 2019. URL: https://doi.org/10.1561/2500000045.
  14. Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman. Ornaments for proof reuse in coq. In 10th International Conference on Interactive Theorem Proving (ITP 2019), pages 26-1. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact