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. For example, consider the theorem that sqrt(2) is irrational. This algorithm examines the statement and its proof, and by checking which lemmas in the proof are used, determines that the only property of 2 used in the proof is that it is prime. So, the algorithm produces a more general statement: that sqrt(p) is irrational, where p is any prime. Note, however, that the algorithm does not derive the more generally true theorem — that the square root of any number that is not a perfect square is irrational — when that reasoning step is not evident in the proof term. Roughly speaking, the algorithm generalizes the theorem only as far as the proof allows. We refer to this type of generalization as proof-based generalization.

=== Hybrid talk ===

Join Zoom Meeting https://cam-ac-uk.zoom.us/j/89856091954?pwd=Bba77QB2KuTideTlH6PjAmbXLO8HbY.1

Meeting ID: 898 5609 1954 Passcode: ITPtalk