Request for examples: verifying vs understanding proofs

Question

My colleague and I are researchers in philosophy of mathematical practice and are working on developing an account of mathematical understanding. We have often seen it remarked that there is an important difference between merely verifying that a proof is correct and really understanding it. Bourbaki put it as follows:

[E]very mathematician knows that a proof has not really been “understood” if one has done nothing more than verifying step by step the correctness of the deductions of which it is composed, and has not tried to gain a clear insight into the ideas which have led to the construction of this particular chain of deductions in preference to every other one.
_{[Bourbaki, ‘The Architecture of Mathematics’, 1950, p.223]}

We are interested in examples which, from the perspective of a professional mathematician, illustrate this phenomenon. If you have ever experienced this difference between simply verifying a proof and understanding it, we would be interested to know which proof(s) and why you did not understand it (them) in the first place. We are especially interested in proofs that are no longer than a couple of pages in length. We would also be very grateful if you could provide some references to the proof(s) in question.

We are sorry if this isn’t the appropriate place to post this, but we were hoping that professional mathematicians on MathOverflow could provide some examples that would help with our research.

Answer 1

Don Zagier has a well-known paper, A one-sentence proof that every prime $p\equiv 1\pmod 4$ is a sum of two squares. An undergraduate mathematics major should be able to verify that this proof is correct. But as you can see elsewhere on MathOverflow, most professional mathematicians are unable to "understand" this proof just by studying it in isolation. By lack of "understanding" is meant, for example, the inability to answer questions such as, "Where did those formulas come from? How did anybody ever come up with this proof in the first place? Is there some general principle on which this proof is based, that is not being presented explicitly in the proof?"

Answer 2

Ivan Niven has published A simple proof that $\pi$ is irrational. Verifying that the proof is correct requires only elementary calculus. On the other hand, to "understand" it, a professional mathematician will probably need to study some general theory (what sort of general strategies are there for constructing an irrationality or transcendentality proof?) and/or some of the history of the subject. Otherwise, it looks like some complicated formulas are being pulled out of nowhere.

Answer 3

"In the remaining sections of this paper we briefly discuss various occurrences of the stability and pinching phenomena in differential geometry. The results we present are, for the most part, not new and we do not provide the detailed proofs. (These can be found in the papers cited in our list of references). What may be new and interesting for non-experts is an exposition of the stability/pinching philosophy which lies behind the basic results and methods in the field and which is very rarely (if ever) presented in print. (This common and unfortunate fact of the lack of an adequate presentation of basic ideas and motivations of almost any mathematical theory is, probably, due to the binary nature of mathematical perception: either you have no inkling of an idea or, once you have understood it, this very idea appears so embarrassingly obvious that you feel reluctant to say it aloud; moreover, once your mind switches from the state of darkness to the light, all memory of the dark state is erased and it becomes impossible to conceive the existence of another mind for which [the] idea appears non-obvious.)" --Mikhail Gromov, "Stability and Pinching" pp. 64-65. Bold emphasis added.

Answer 4

From a logic viewpoint, verifying a proof is a syntactic business, also known as symbol pushing, whereas understanding a proof is a semantic matter. I cannot resist giving a layman analogy as an appetizer: Many people can follow a recipe to bake a cake, but not as many can design the recipe or know how to tweak it to make something else.

Many of the best examples involve the proof of an existential statement that requires constructing a complicated witness for it. You may be familiar with the construction of the reals via Dedekind cuts of rationals or via Cauchy sequences of rationals, and these proofs can be easily checked step by step by any student who understands some basic mathematics, but how many students truly understand these constructions? Do they know that the Dedekind cut approach extends to completion of linear orders, while the Cauchy sequence approach extends to completion of metric spaces? Do they get some sense of wonder that both ways happen to produce the same result in the case of completing the rationals?

In a similar vein, one can construct the complex numbers by defining them to be the set $C = \mathbb{R}^2$ with $+,·$ defined by $(a,b)+(c,d) = (a+c,b+d)$ and $(a,b)·(c,d) = (ac-bd,ad+bc)$, and then checking that $(C,+,·,(0,0),(1,0))$ is a ring and that $(a,b)·(\frac{a}{\sqrt{a^2+b^2}},-\frac{b}{\sqrt{a^2+b^2}}) = (1,0)$ for every $(a,b) ∈ C ∖ \{(0,0)\}$. But in my view this proof ought to feel mysterious and unsatisfying unless you actually understand the motivation for these definitions and know the construction via field extension (i.e. $R[X]/(X^2+1)R[X]$). This is because there is a priori no reason at all for the above definitions of $+,·$ to make $·$ associative and distributive over $+$, unless you already understood that the reals can be extended to a field with some element $i$ such that $i^2+1 = 0$, and that the resulting field must be a vector space over the reals with dimension $2$, which together force $+,·$ to necessarily obey those definitions! Otherwise, you would be totally in the dark as to why those definitions should work, even though you can plainly see that they do.

These are examples from basic mathematics, but I hope it demonstrates how an existential statement might have a proof that does not in itself provide any understanding of the proof, in the same way you might observe that the cake mixture rises upon baking without having a clue why it does...

As for personal experience, there is one particular proof that I have never felt I really understood, even though I have a solid grasp of the formal proof itself: $ \def\pa{\text{PA}} $

Theorem: Let $T = \pa + \{ \ c>1 \ , \ c>1+1 \ , \ c>1+1+1 \ , \ \cdots \ \}$, where $c$ is a fresh constant-symbol. Then $T$ is conservative over $\pa$.

Proof: Take any arithmetical sentence $Q$ such that $\pa ⊬ Q$. Then $\pa+¬Q$ is consistent and so has a model (by completeness), which clearly finitely satisfies $T+¬Q$, and hence $T+¬Q$ has a model (by compactness). Thus $T ⊬ Q$.

Although I completely understand the completeness and compactness theorems, I somehow cannot intuitively understand how this proof works. Why should we have to invoke models? Can we instead directly show that every proof of any arithmetical $Q$ over $T$ can be converted into a proof of $Q$ over $\pa$?

Answer 5

Doron Zeilberger's proof of the alternating sign conjecture is perhaps an extreme case of this. He enlisted a large team of referees (88 apparently) to each verify a small part of the long but rather modular proof. A shorter and presumably more conceptual proof was later given by Kuperberg, and Zeilberger then used Kuperberg's methods to prove a refined version of the conjecture. No one of the referees could be said to understand the proof. Arguably, Zeilberger didn't have a good understanding of why the conjecture was true, past the nearly 100 elementary steps, since the second proof seems to have illuminated the conceptual concepts, leading to a proof of a stronger statement.

Answer 6

One such (rather unremarkable) example is the proof at https://mathoverflow.net/a/239931/36721, which I wrote myself, but now don't remember how it was devised. So indeed, I don't really understand it. :-)

Answer 7

Sergey Pinchuk gave a counterexample to the Real Jacobian Conjecture (that every polynomial map from $\mathbb{R}^n$ to itself whose jacobian determinant is everywhere nonvanishing is invertible). The verification is by high school level algebraic manipulations and takes 2 pages (the whole paper is less than 4 pages). But of course it does not give a clue about how he came up with the map. As he states in the paper, "The most difficult (and invisible) part of the present construction was to find polynomials $t$, $h$, $f$ with nontrivial Newton diagrams and satisfying Abhyankar's condition."

Answer 8

One example in logic is the proof that $A \Longrightarrow A$ in a "Hilbert-style" deduction system, where our only inference rule is Modus Ponens and we have the two axiom schemata

• K: $\beta \Longrightarrow (\alpha \Longrightarrow \beta)$
• S: $(\alpha \Longrightarrow (\beta \Longrightarrow \gamma)) \Longrightarrow ((\alpha \Longrightarrow \beta) \Longrightarrow (\alpha \Longrightarrow \gamma))$

What gibberish are these? Well, it turns out those are precisely what you need to prove the Deduction Theorem for these systems — that if $\alpha \vdash \beta$ (using $\alpha$ as hypothesis, one can prove $\beta$) then $\vdash \alpha \Longrightarrow \beta$ (with no hypotheses, one can prove $\alpha \Longrightarrow \beta$) — by providing an algorithm that transforms any proof of $\alpha \vdash \beta$ into a (three times as long) proof of $\vdash \alpha \Longrightarrow \beta$. The idea is that for any step $\gamma$ in the original proof, you have a step $\alpha \Longrightarrow \gamma$ in the transformed proof, and then you have a bunch of extra steps to make it all fit together. Axiom scheme S is precisely what you need in order to do a modus ponens $\beta \Longrightarrow \gamma, \beta \vdash \gamma$ when there is a $\alpha \Longrightarrow$ prefix on everything. Axiom scheme K lets you put that $\alpha \Longrightarrow$ prefix on things that are theorems anyway, to import them into the hypothetical realm. However, that part is just definitions / an axiom system, not the mysterious theorem.

To complete the proof transformation required for the Deduction Theorem, you do however also need to prove that $\vdash \alpha \Longrightarrow \alpha$, since this is what you get as the transformation of the step where your proof uses the hypothesis for the first time. Frege had this as a separate axiom ($\alpha \Longrightarrow \alpha$ is a tautology, as he did for K and S, rather than prove it from earlier theorems as he did for everything else (in the implicational fragment of propositional calculus).">at least sort of), but it turns out it can be proved from schemata K and S alone, in just five steps:

1. $(A \Longrightarrow ((A \Longrightarrow A) \Longrightarrow A)) \Longrightarrow ((A \Longrightarrow (A \Longrightarrow A)) \Longrightarrow (A \Longrightarrow A))$
   • instance of axiom scheme S, with $\alpha = \gamma = A$ and $\beta = A \Longrightarrow A$
2. $A \Longrightarrow ((A \Longrightarrow A) \Longrightarrow A)$
   • instance of axiom scheme K, with $\alpha = A \Longrightarrow A$ and $\beta = A$
3. $(A \Longrightarrow (A \Longrightarrow A)) \Longrightarrow (A \Longrightarrow A)$
   • from 1 and 2 by modus ponens
4. $A \Longrightarrow (A \Longrightarrow A)$
   • instance of axiom scheme K, with $\alpha = \beta = A$
5. $A \Longrightarrow A$
   • from 3 and 4 by modus ponens

Checking that this is a proof is trivial. Explaining how it works… is a different matter entirely.

Enter the Curry–Howard correspondence

The names K and S are not from formalised logic, but from the combinatory calculus: these are the standard names for the two higher order functions satisfying the identities

• $K(x)(y) = x$
• $S(f)(g)(x) = f(x)(g(x))$

TeXheads may prefer to think of those as the TeX macros that would be defined as

\def\K#1#2{#1}                % A.k.a. \@firstoftwo
\def\S#1#2#3{#1{#3}{#2{#3}}}  % Not a common utility, but should be

The fun thing about those two is that they generate the whole combinatory calculus — any lambda-term whatsoever can be mechanically translated to a composition of $K$ and $S$. In particular the identity function $I(x)=x$ can be so expressed, in the sense that

• $S(K)(K)(x) = K(x)(K(x)) = x$ for all $x$, hence $I = S(K)(K)$.

Now the untyped combinatory calculus, like the untyped lambda calculus, is too powerful for many purposes (it lets you do anything), so a major activity in these parts of logic and foundations of computer science is to tame it by stamping types on everything. The basic system is the simply-typed theory, where you have some set of atomic types and the ability to make function types; $f : \alpha \to \beta$ means $f$ is a function that takes an argument of type $\alpha$ and returns an argument of type $\beta$. To get functions of several variables, you use currying, so instead of some $f : \alpha \times \beta \to \gamma$ you have $f : \alpha \to (\beta \to \gamma)$. For example the $K$ combinator has type $\alpha \to (\beta \to \alpha)$ since its result has the same type ($\alpha$, say) as the first argument whereas its second argument can have any type ($\beta$).

Similarly analysing the defining identity $S(f)(g)(x) = f(x)(g(x))$ of $S$, we may arbitrarily let $x : \alpha$ (we pick the name $\alpha$ for the type of $x$). Then $f$ and $g$ must both have some $\alpha \to$ type, as they both take $x$ as their first argument. $f(x)$ take $g(x)$ as its argument, but the type of $g(x)$ is not constrained, so let's call that $\beta$, making $g : \alpha\to\beta$. The type of $f(x)(g(x))$ is likewise not constrained, so let's call that $\gamma$. Then we get

• $f : \alpha \to (\beta \to \gamma)$
• $S : (\alpha \to (\beta \to \gamma)) \to ((\alpha\to\beta) \to (\alpha\to\gamma))$

Simply typed terms are too restrictive for proper programming — you can only write trivial programs — so there is an entire industry of designing more complicated type systems for doing more (though still less than the untyped calculus can) while still keeping the functions tame; at least this gives the theorists something to do. However we will only need to consider the $S(K)(K)$ expression for the identity, which is perfectly possible to type with simple types, provided one observes that we can't use the same types for the two $K$s (they will be two different instances of the same untyped combinator). If we take $A$ to be the concrete type of some $x$ that our $S(K)(K)$ should apply to, then the second $K$ must fit the pattern for a $g$ argument of $S$ and have a type of the form $A \to (B \to A)$ for some (so far not constrained) type $B$. The first $K$ must take $x$ as its first argument and $g(x) : B \to A$ as its second, so the first $K$ rather has type $A \to ((B \to A) \to A)$. This means $\alpha = \gamma = A$ and $\beta = B \to A$ in the typing of $S$, so our typed identity of type $A \to A$ is in fact

• $S_{(A \to ((B \to A) \to A)) \to ((A \to (B \to A)) \to (A \to A))} ( K_{A \to ((B \to A) \to A)} )( K_{A \to (B \to A)} )$

where the indices show the exact type instance of the three combinators that is at hand.

As it turns out, that combinatory term also serves as a blueprint for the above proof that $A \Longrightarrow A$, because the instances of the axiom schemes K and S have exactly the same structure as the possible types of the combinators $K$ and $S$, if one substitutes the implication arrow $\Longrightarrow$ for the function type arrow $\to$ (and for simplicity replaces $B$s by $A$s as well). Modus ponens has the same structure as the type inference "if $x$ has type $\beta$ and $f$ has type $\beta \to \gamma$, then $f(x)$ has type $\gamma$". This is (an elementary instance of) the Curry–Howard correspondence.

Opinions vary as to whether this is is a Deep Insight into the way logic really works, or just a funny coincidence. People can get ideological about it. For me, the only way I can reproduce that 5 step proof is to derive it by assigning types in $S(K)(K)$.

Answer 9

Maybe the fact that the Jones polynomial is a well-defined invariant of knots qualifies. If you're willing to accept Reidemeister theorem, whose proof is itself somewhat easy to follow though more delicate than one might think, then using the skein relation this is really straightforward and can be explained to someone with no mathematical background and basically boils down to drawing pictures. So checking that it works is easy, but the fact that it works is fairly miraculous, and understanding this involves some deep mathematics.

Answer 10

For myself, I would mention the Lee-Yang theorem (see a mathoverflow post here or the book of David Ruelle "STATISTICAL MECHANICS Rigorous Results".

I admit that I have checked the proof many times. But I still don't really understand what happens there nor have any physical insight why this result should be true.

Answer 11

A variation on this is the "not rediscoverable proof". This is a proof of a result which you can verify, and perhaps even understand why it is a proof, but which you could not discover on your own just given the theorem statement. I think this arises from studying an area, and then finding a surprising and unexpected consequence. Perhaps this speaks more to the nature of understanding, in that a deductive consequence come as such a surprise.

The amazing example of this I have found is Lovasz's cancellation theorem for finite structures, from one of his first published papers. Even after having reviewed the proof many times, I still could not imagine how I could come up with it. More technical detail can be found in an answer of Eric Wolsey, with some of my commentary nearby. https://mathoverflow.net/a/269545/ .

Gerhard "Understands Understanding Isn't Very Understandable" Paseman, 2020.06.12.

Answer 12

A good proof is a proof that makes us wiser. If the heart of the proof is a voluminious search or a long string of identities, it is probably a bad proof. If something is so isolated that it is sufficient to get the result popped up on the screen or a computer, then it is probably not worth doing. Wisdom lives in connections. If I have to calculate the first 20 digits of π by hand I certainly become wiser afterwards because I see that these formulas for π that I knew take too much time to produce 20 digits. I will probably devise some algorithms which minimize my effort. But when I get two millions of digits of π from the computer using somebody else's library program I remain as stupid as I was before.

Yuri I. MANIN, Good Proofs are Proofs that Make us Wiser

Answer 13

While I agree very dearly with erz's comment that every mathematical result/proof/... is like that, I also think that there are some examples that showcase this better than other ones.

A large portion of commutative algebra would make for a good example. It is not too hard to verify many of the standard textbook results but to really understand the arguments, one might need to think about related theories like algebraic geometry.

It is not too bad to verify proofs of Noether Normalization or Lying Over or Insert More Examples but what do they really mean? It is easy to verify that affine varieties induce morphisms of algebras and vice versa algebra-homomorphisms between coordinate rings induce morphisms of varieties. And it is easy to prove/verify that they are compatible in a natural way. But when I studied these things in my second year at university I didn't understand why we wanted to prove this or why we should even expect this to work.

After learning just the fundamentals of category theory and bits of geometry, however, one would realize that there is some algebro-geometric correspondences going on and that this is just the most natural way of defining an equivalence of categories, so of course it had to work.

Some of this might not even be considered "verifying a proof" but rather "verifying a definition" - which clearly should happen even more often, since it is oftentimes easy to "verify" a definition but years have gone into the development of the definition. (I'm thinking of the definition of a topology, or e.g. definitions of model category and $\infty$-categories, and so on and so on.)

Answer 14

A Robbins algebra is an algebra including a single binary relation satisfying associativity, commutativity, and the "Robbins axiom" $\neg \left( \neg \left(a \lor b \right) \lor \neg \left(a \lor \neg b \right) \right) = a$.

McCune's proof that Robbins algebras are synonymous with Boolean algebras is a relatively famous application of computer-assisted automated theorem proving; the output of the computer was small enough to be checked "by hand". This is on the "flip-side" of, for example, the Four-Color Theorem, wherein the output is likely not human-readable and more trust must, in a sense, be placed in the computer.

My limited understanding is that, although human-readable, the proof per se lacks intuition - it isn't clear how a human could have come up with the proof of the Robbins conjecture.

Answer 15

George Boolos wrote a paper entitled Gödel's Second Incompleteness Theorem Explained in Words of One Syllable wherein, indeed, he does explain the second incompleteness theorem using only words of one syllable. I am not sure if the monosyllabic explication offered in the beginning of the paper is an example of verifying a proof, as the explication more or less just states results as opposed to proving them or even sketching what the proofs look like. However, I believe that the second half of the paper fills in enough of the details for any mathematician to follow the proof and verify the result, but lacks enough of the formal definitions and technical machinery to allow someone to fully understand the proof. A mathematician who has no background in mathematical logic reading this paper could easily verify the proof on the third page starting from "We may prove Gödel's second incompleteness theorem," but I highly doubt they could give an explanation of what is really going on 'under the hood' of the proof, or any of the corollaries and consequences of the theorem, nor do I think would they be able to use the same techniques used in this proof to prove other results in computability theory or proof theory just from reading this paper alone.