54
$\begingroup$

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.

$\endgroup$
14
  • 8
    $\begingroup$ Cantor's diagonal argument (or in general Cantor's theorem) is a very popular example of a theorem whose proof is extremely easy to verify, but it takes some students (and amateurs) quite some time to fully digest and understand it. This is one of the reason "counterexamples to Cantor's theorem" are so frustrating, because it's always so easy to throw the "counterexample" against the proof and see it fails. $\endgroup$
    – Asaf Karagila
    Jun 9, 2020 at 16:52
  • 3
    $\begingroup$ I think that Charles Fefferman said that he checked Kuranishi's proof of CR embedding line by line, but could never understand what made it work. $\endgroup$
    – Ben McKay
    Jun 9, 2020 at 16:53
  • 48
    $\begingroup$ Conversely, it's possible to understand a proof without verifying all the details! I think this situation is much more common for working mathematicians. $\endgroup$ Jun 9, 2020 at 16:57
  • 6
    $\begingroup$ I am sorry for an unhelpful comment, but literally every proof is like that. I think you can even find good examples among answers to MathOverflow questions. $\endgroup$
    – erz
    Jun 9, 2020 at 17:53
  • 3
    $\begingroup$ I would view a proof like a path from A to B. Verifying the proof behaves like walking along that path and understanding the proof is more like understanding at each intersection, why one chooses a specific direction and whether there are any short-cuts. $\endgroup$ Jun 10, 2020 at 7:47

15 Answers 15

52
$\begingroup$

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?"

$\endgroup$
1
  • 22
    $\begingroup$ I am one of those at MO who has complained about this proof. However, I was shown the light about what is really going on there by this pretty wonderful Mathologer video on youtube: youtube.com/watch?v=DjI1NICfjOk. (Oh, and now I see that Moritz Firsching explained the same thing in the other thread.) $\endgroup$
    – Todd Trimble
    Jun 9, 2020 at 19:17
31
$\begingroup$

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.

$\endgroup$
27
$\begingroup$

"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.

$\endgroup$
3
  • 2
    $\begingroup$ I find this same phenomenon sometimes makes it difficult to write papers (I'm a physicist, not a mathematician though), because after having worked on a problem for a long time one loses perspective since after the fact the results may seem almost trivial $\endgroup$
    – Kai
    Jun 11, 2020 at 2:06
  • 2
    $\begingroup$ @Kai Indeed! I also find it to be an important aspect to grapple with when teaching: we are often too familiar with the given subject and need to actively empathize with out students, to remind ourselves that we too did not always find a subject trivial. $\endgroup$
    – erfink
    Jun 11, 2020 at 3:31
  • 2
    $\begingroup$ I don't completely agree with that quote. The "enlightenment" process in question is quite personal, and the goal is to make (or accelerate) others understand, not to repeat my "enlightenment" process in another individual. Teaching is even more difficult: you need to know how to make a large variety of different students understand. The difficulty is not solely explained by "forgetting one's own dark state". $\endgroup$
    – user20948
    Jun 12, 2020 at 10:39
22
$\begingroup$

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$?

$\endgroup$
2
  • 8
    $\begingroup$ No models are needed for the conservativity of T over PA. Given a proof in T of an arithmetical Q, let $n$ be larger than all the (finitely many) numbers $m$ such that $c>1+1+\dots+1\ \ (m$ summands) was used in the proof. Throughout the proof, replace $c$ with $1+1+\dots+1\ \ (n$ summands), and you have (modulo trivialities) a proof of Q in PA. $\endgroup$ Jun 10, 2020 at 15:54
  • 1
    $\begingroup$ @AndreasBlass: Oh that's so simple, thanks! $\endgroup$
    – user21820
    Jun 10, 2020 at 17:46
14
$\begingroup$

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.

$\endgroup$
5
  • 1
    $\begingroup$ Here are the referee reports, which make for interesting reading! sites.math.rutgers.edu/~zeilberg/asm/REPORTS $\endgroup$
    – David Roberts
    Jun 10, 2020 at 10:35
  • 2
    $\begingroup$ This doesn't meet the criterion of being just a couple of pages long. If we allow this type of example then there are tons of examples of extremely computational proofs that only a computer can verify, and nobody "understands" except at a high level (four color theorem, Flyspeck, checkers is a draw, various results in extremal combinatorics, etc.). $\endgroup$ Jun 10, 2020 at 11:48
  • 3
    $\begingroup$ Here the distinction is between proof P and proof Q of the same resultThe question involves the distinction between verifying and understanding proof P. It can’t always be said that understanding proof Q increases understanding of proof P. $\endgroup$ Jun 10, 2020 at 16:12
  • 4
    $\begingroup$ @AaronMeyerowitz : Yes, that's a very good point. Kuperberg's proof gives additional insight into the theorem, but I don't think it helps anyone "understand" Zeilberger's proof; it's a completely different proof. $\endgroup$ Jun 10, 2020 at 17:36
  • 1
    $\begingroup$ OK, I didn't see that requirement. But it's an interesting corner case. I agree that the proofs are different, as Zeilberger himself explains (his proof gives something stronger that Kuperberg's doesn't). But there are cases where an old elementary proof is known to be essentially the same as a new high-powered but more conceptual proof. Consider for instance things in number theory dating back to Fermat that are implicitly about constructing points on elliptic curves. Or proving no such points exist by infinite descent. $\endgroup$
    – David Roberts
    Jun 11, 2020 at 0:39
10
$\begingroup$

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. :-)

$\endgroup$
10
$\begingroup$

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."

$\endgroup$
8
$\begingroup$

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)$.

$\endgroup$
4
  • 1
    $\begingroup$ Perfect example. I just read this and immediately I fall back to not understanding the point of the Deduction Theorem. How could it not be the case? How would you even think that it is a thing to doubt? $\endgroup$
    – Mitch
    Jun 12, 2020 at 19:22
  • 1
    $\begingroup$ @Mitch : Surely as soon as one grasps the distinction between $\vdash$ and $\implies$ one is led to ask what the relationship between them is? $\endgroup$ Jun 12, 2020 at 21:17
  • $\begingroup$ @TimothyChow. Of course. $\rightarrow$, $\Rightarrow$, $vdash$, $\vDash$ all so distinct. But sometimes you just... it's all so... just look at them... side by side... it's so obvious! $\endgroup$
    – Mitch
    Jun 13, 2020 at 17:48
  • 1
    $\begingroup$ @Mitch: It's obvious on the semantic side, but formalised logic is about what you can establish on the syntactic side. Gödel couldn't arithmetise the concept of truth, because that is semantic, but he could arithmetise the concept of provability because that is (in the modern view) strictly syntactic. $\endgroup$
    – Lars H
    Jun 14, 2020 at 13:54
5
$\begingroup$

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.

$\endgroup$
4
  • $\begingroup$ Isn't the same true of most knot invariants? Especially the ones like this one which are given in terms of the knot diagrams $\endgroup$
    – Wojowu
    Jun 9, 2020 at 22:26
  • $\begingroup$ @Wojowu Not, e.g., the Alexander polynomial. $\endgroup$
    – Will Sawin
    Jun 9, 2020 at 22:53
  • 1
    $\begingroup$ @Wojowu the same case could be make about the HOMFLY polynomial, but apart from that all the "classical" knot invariants are either super elementary or have a clear topological definition (or both) e.g. knot group, linking number, crossing number,... On the other hand, others "quantum" invariant do not have such a simple rule to compute them, the only exception being the Alexander polynomial which in a way is both classical and quantum, and as Will say does have a clear topological meaning. $\endgroup$
    – Adrien
    Jun 10, 2020 at 8:23
  • $\begingroup$ @Adrien Thank you, I'm showing off my ignorance in the field of knot theory; my little experience with the field is through the more elementary invariants presented via knot diagrams. Sometimes I'm forgetting knot theory is a subfield of topology and not combinatorics :) $\endgroup$
    – Wojowu
    Jun 10, 2020 at 9:03
4
$\begingroup$

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.

$\endgroup$
4
$\begingroup$

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.

$\endgroup$
4
$\begingroup$

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

$\endgroup$
3
$\begingroup$

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.)

$\endgroup$
1
  • $\begingroup$ It is rather frequent that results on algebra get illuminated by geometry. For me, this is "understanding" of the commutative algebra facts. But, for some people the geometric view just adds another layer of confusion. $\endgroup$
    – Leo Alonso
    Jun 11, 2020 at 16:28
3
$\begingroup$

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.

$\endgroup$
1
  • 1
    $\begingroup$ I expect that a human, or group of humans, could have come up with a proof of this by doing reams and reams of inferences from axioms. It's not so much the presence of the computer that induces the lack of intuition, but the manner in which the proof was constructed. $\endgroup$ Jun 11, 2020 at 18:36
2
$\begingroup$

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.

$\endgroup$
1
  • 1
    $\begingroup$ To add to this, I have never seen one of these "In words of one syllable..." or "In words of two syllables or less..." things that did not end up acting as a reductio ad absurdum of requests to express things in layman's terms. That is to say, putting such restrictions only makes things harder to understand for beginners, more opaque and less motivated. The problem is that when people don't understand something, they don't know how to ask for help with understanding it that they can actually use. $\endgroup$ Jun 11, 2020 at 18:33

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.