Automatically Generalizing Proofs and Statements

Often, generalizing all instances of a constant in a theorem to the same variable yields unnatural generalizations. Consider, for example, the following result.

Sometimes when mathematicians say that they wish to generalize a constant $c$, they really need to generalize not just occurrences of $c$, but also occurrences of other constants in the proof that depend on $c$. For example, consider the following theorem, which bounds the size of the union of two sets.

It often happens that proofs contain deductions about a constant that are specific to that constant and therefore need to be abstracted away as hypotheses in the generalization. Pons’s algorithm is able to identify such hypotheses when they are present in the form of lemmas, but fails when a fact about a constant is encoded in an arbitrary sub-portion of the proof.

Consider the following proof.

The working of the algorithm can be summarized as follows. The algorithm takes as input a proof and a constant to generalize in it and begins by traversing the proof, replacing occurrences of that constant with metavariables (which can be thought of as placeholders or holes).²²2Note that the default generalization produced is not minimal, since the procedure here abstracts all occurrences of the constant being generalized (unless the “occurrences” flag is passed to the tactic, specifying which occurrences are to be generalized). In particular, this means that if two occurrences of a constant are coincidentally equal, then the default output is different from what it would be if they were not equal. There may be portions of the proof which use specific properties and facts about this constant that are not generalized by this process; they must be separately abstracted out as hypotheses.

The algorithm then outputs a generalized version of the theorem together with a proof. Note that since the algorithm operates on and modifies the proof term, the tactical structure of the proof is not preserved.

A diagram summarizing the algorithm is below.

Each stage in the above diagram is described in detail in the following section.

We now turn to describing the algorithm in more detail. For clarity, we present the algorithm in various stages, some of which actually take place simultaneously in a single pass through the proof to be generalized.

If a proof relies on two types being definitionally equal, it will fail to be typecorrect after generalization if the definitional equality no longer holds, as shown in the following example.

The first step of the proof relies on the fact that $a\mid b$ is defined as $\exists c\in \mathbb{Z},c\ast a=b$ over the integers. That is, Lean considers $a\mid b$ to be definitionally equal to $\exists c\in \mathbb{Z},c\ast a=b$, and therefore can switch between the two without explicit conversion in the proof. When the integers are generalized to a different type, the following proof (which doesn’t explicitly expand the definition of $a\mid b$) breaks since the division symbol “$\mid$” is not necessarily defined the same way for an arbitrary type carrying a division operation.

So, when the tactic attempts to operate on the proof term to generalize the theorem, the generalized proof cannot make use of any definition of division, and therefore does not typecheck. Again, as mentioned earlier, since the tactic never produces incorrect generalizations, “failure” in this case means the tactic produces a typechecking error, and returns no generalized proof.

Explicitly expanding the definition of division with a rewrite fixes this issue,⁴⁴4Note that the tactic unfold does not change the proof term at all – it simply changes the goal visible to the user to a definitionally equal goal. adding an extra hypothesis $\forall a,b\in T,(a\mid b)=\exists c,b=a\ast c$ to the generalization (where $T$ is the type $\mathbb{Z}$ is being generalized to).

Future work on the algorithm will include building in automatic detection of when such definitional equalities are used in the proof, and the insertion of these as hypotheses, to facilitate generalization.

There are often multiple ways to prove the same theorem, and often each proof will generalize in a different way. This is a phenomenon also encountered by mathematicians when they generalize pen-and-paper theorems.

For example, suppose we wish to generalize the statement that $\sqrt{2}$ is irrational with a view to showing that $\sqrt{m}$ is irrational under suitable conditions on $m$. If the proof we choose when $m=2$ appeals to the fact that every odd number can be written in the form $2k+1$, then the natural generalization will appeal to the fact that every non-multiple of $m$ can be written in the form $mq+r$ with . If instead, it observes that $2$ is prime and uses that to prove that if $a^2$ is a multiple of 2, then so is $a$, then the natural generalization of the proof will yield the statement that the square root of every prime number is irrational. And if the proof instead observes that $2$ occurs an even number of times in the prime factorization of $a^2$ and an odd number of times in the prime factorization of $2b^2$, then the natural generalization will yield the statement that $\sqrt{m}$ is irrational if $m$ is not a perfect square.

When generalizing a statement for which one has a proof, it is often desirable to modify the proof to make it more suitable for further generalization, by trying as far as possible not to use specific facts about the constants one is generalizing. Our algorithm does not perform pre-processing of this kind: we envisage it as a component of a more sophisticated generalizer that might be capable of doing so, but that is for future work.

Because proof generalization relies on a thorough examination of the proof, it benefits the generalization if every step of the proof is evident in the proof term. A limitation of any proof-generalization tool, and therefore of this algorithm in particular, is that black-box steps can obscure some parts of the proof and therefore yield suboptimal generalizations.

Often such steps take the form of small computations. Consider, for example, the following problem, which appeared in Round 2 of the British Mathematical Olympiad in 1993.

It is natural to begin by looking at the simplest case, namely $p=5$. In this case $m=(2^{10}-1)/3=341$, so the problem requires us to show that $2^{340}$ leaves a remainder of 1 when divided by $341$, or equivalently that $2^{340}\equiv 1(mod341)$.

A phenomenon that seems relevant is that $2^{10}\equiv 1(mod{2}^{10}-1)$, and indeed that quickly implies that $2^{10}\equiv 1(mod341)$. But that gives us what we want, since $10$ divides $340$.

If we now try to generalize this argument by replacing $5$ with a general prime $p>3$, everything works smoothly apart from at the very end, where in place of the observation that $10$ divides $340$ we need to prove that $2p$ divides $(4^p-1)/3-1$. When $p=5$ we proved this computationally: we just noted that $340=34\times 10$. That option is not available to us for general $p$ and we have to supply an argument. This turns out not to be too hard, but it is out of the scope of our algorithm. What we can hope for in this case is a proof of the theorem that $2^{m-1}\equiv 1(modm)$ if $2p\mid (4^p-1)/3-1$.

A related, more technical issue arises when computation rules are used in Lean. Suppose that, within the context of a larger proof, it is useful to prove that $2\times 3$ is even. We can prove this either by using deduction rules or by using computation rules. A deductive approach might be to argue that $2$ times any number is even, by definition, and thus that $2\times 3$ is even. A computational approach would be to calculate $2\times 3$, obtaining the answer $6$ (in Lean, this computation could be carried out with the procedure reduceMul), and then to use the fact that $6$ is even. When given the first proof, our generalization algorithm can generalize the $3$ to an arbitrary integer $c$. When given the second proof, our algorithm is unable to find an occurrence of $3$ to generalize, because the Lean proof term does not record that $2\times 3$ was the operation that was done, just that $6$ is the result of the computation. Thus, we can no longer determine which properties of $3$ were used in the proof. And if another part of the proof relies on unification with that $3$, a type error may arise during the generalization.

For our purposes, this is a downside of a language like Lean, which does not show computations in the proof term. But the larger issue (that some programs, not necessarily just theorem proving programs, contain black boxes) is tackled by other languages such as Pientka’s functional programming language Beluga [10], which prioritizes creating only programs that can be transparently reasoned about. Theorems proved in these less opaque languages may be particularly amenable to proof-based generalization.

Imagine that one is developing the theory of real numbers and considering the question of whether the least-upper-bound axiom, together with the axioms for an ordered field, is enough to yield that the number $2$ has a square root. It is natural to consider the supremum $s$ of the set and it turns out not to be too hard to prove that $s^2=2$.

Having done this, one can consider replacing $2$ by a more general real number and the function $x\mapsto x^2$ by a more general function $f$. Performing a proof generalization, one discovers that the argument works provided that $f$ and $c$ obey certain conditions, namely the standard hypotheses for the intermediate value theorem: $f$ should be continuous and there should exist $x$ and $y$ such that and $f(y)>c$.

After performing this generalization, we have a much more general and flexible theorem, which allows us to argue that all sorts of other equations can be solved. For example, if we have defined the exponential function and proved that it is continuous, we can show that for every positive real number $c$ there exists $x$ such that $e^x=c$, which gives us a definition of the logarithm function.

This is a very common phenomenon in mathematics: a lemma proved for a narrow purpose can be significantly generalized (with a proof-based generalization), and becomes useful well beyond its original context.

Consider the following problem.

It is not obvious why such a statement should be true, so one way of gaining some intuition is to look at some special cases. When $p=2$, we observe that

since $2\equiv 0(mod2)$. When $p=3$ we observe similarly that

since $3\equiv 0(mod3)$. And when $p=5$, we find that

since both $5$ and $10$ are multiples of 5.

These simple proofs rely on the fact that all the coefficients we obtain when we expand out ${(x+y)}^p$ are multiples of $p$. However, this is shown computationally, so this fact does not obviously generalize beyond these simple examples, and will therefore not be obtained by a proof-generalization algorithm. Instead, an ideal proof generalizer would output the following conjecture.

It would of course be possible to arrive at this conjecture by simply noting that ${(x+y)}^p$ can be expanded using the binomial formula, that two of the terms are $x^p$ and $y^p$, and that the remaining terms all have coefficients $\left(\genfrac{}{}{0pt}{}{p}{k}\right)$ for some $k$ between 1 and $p-1$. However, our confidence that it is correct is greatly increased by the fact that we have seen (i) that it holds in a few special cases and (ii) that it played an important role in the proof of those cases. In more complicated examples, proof generalization can help to identify conjectures that would be significantly harder to guess than this one.

When mathematicians prove a theorem by induction, often the idea behind how to prove the inductive step $P(n)⟹P(n+1)$ in the general case can be discovered by proving the first few cases, for instance $P(1),P(2)$ and $P(3)$, and using proof generalization. Of course, if that is one’s strategy, then in the course of proving $P(3)$ one will try to make use of $P(2)$, so that the proof has a good chance of generalizing appropriately.

As we saw in the generalization of Bézout’s theorem in Section 5, one of the uses of proof generalization is to formulate useful new abstractions, by examining proofs about concrete objects and identifying the properties of those objects that are essential to the proofs.

In practice, the most useful abstraction of a proof is not always the most general. An interesting avenue that we have not yet explored would be to start with two proofs and aim to find something like a least common generalization. For example, one could begin with Bézout’s theorem for integers and for polynomials: the weakest natural simultaneous generalization of those two results might well yield precisely the definition of a Euclidean domain, rather than the more general structure that our algorithm provides (which, for instance, is not necessarily an integral domain).

A fundamental part of the process of solving mathematical problems is conjecturing potentially useful intermediate lemmas, and refining one’s conjectures if they turn out to be false. Proof generalization is an important component of this kind of “learning from failure.” Suppose, for example, that one wishes to prove a statement of the form $\forall x\in X,P(x)⟹Q(x)$. Sometimes, one may identify a property $R$ that is easily seen to be stronger than $Q$, and conjecture that in fact $\forall x\in X,P(x)⟹R(x)$. If we then discover some $z\in X$ such that $P(z)$ is true but not $R(z)$, then instead of simply abandoning the conjecture, we can attempt to generalize the proof of the statement $P(x)\wedge \neg R(z)$, obtaining a class of solutions. This we can express as a statement of the form

If now we would like to have another try at finding a property $T$ such that $P⟹T$ and $T⟹Q$, we know in particular that $S$ should imply $T$, which is a more stringent condition than the condition that $z$ should satisfy $T$. Thus, the proof generalization has helped us to reduce the size of our search space.

Details, illustrated with several examples, will be given in a future paper by the authors.⁶⁶6The phrase “learning from failure” is often used differently in the automated theorem proving community, with the word “failure” referring to an invalid proof of some statement, and “learning from failure” meaning patching that proof. Tools like Ireland and Bundy’s [6] have been used to perform this patching and to learn from failure in this alternative sense. For our purposes, “failure” is a valid disproof of a conjecture, and we can “learn from failure” by generalizing that disproof.

An important challenge in automatic theorem proving is designing systems that do not just answer questions but ask them, with the important caveat that the questions they ask should be natural and interesting. Current methods tend to work in a rather “computery” way, for example asking a large number of questions in some domain and filtering out the ones that have easy answers. This is quite unlike the approach that human mathematicians take. In particular, human mathematicians often come up with interesting questions as a result of refining conjectures that arise naturally when they are thinking about other questions. As several of the examples discussed in this paper illustrate, proof generalization is one of the ways in which one question can lead to another that is recognisably “motivated”, and therefore interesting.

We have already seen an indication of how this process can work: when trying to generalize the proof that $\sqrt{2}$ is irrational, an ideal algorithm outputs the condition “For every $a$, if $n\mid a^2$ then $n\mid a$,” which can be converted into the problem, “For which positive integers $n$ is it the case that for every $a$, if $n\mid a^2$, then $n\mid a$?” which can in turn lead on to many other interesting questions that did not have an immediately obvious relationship to the irrationality of $\sqrt{2}$.

For this reason it seems likely that proof generalization will be at the heart of any system that is good at generating interesting mathematical questions.