2026-08-18T08:42:02Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:24610 2025-12-12T15:09:56Z ddc:004 open_access

Automatically Generalizing Proofs and Statements Gandhi, Anshula Tadipatri, Anand Rao Gowers, Timothy automated reasoning automated theorem proving interactive theorem proving formalization of mathematics generalization Lean theorem prover Lean tactic 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Anshula Gandhi and Anand Rao Tadipatri and Timothy Gowers 2025 Is Part Of LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2025.12 urn:nbn:de:0030-drops-246104 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.12 eng https://creativecommons.org/licenses/by/4.0/legalcode