Your proof is not my proof

Jennifer Chayes is theorist who has made fundamental contributions in two different ways, some directly as a researcher and some indirectly as a manager. She is the director and co-founder of the Microsoft research lab in Cambridge—the one in New England—not England. Her main research contributions are in the area that spans theory and physics, including phase transitions in discrete systems such as networks. Her main administrative contributions have been in the creation of world class teams. Each of these types of contributions is impressive and each is hard—I think it takes a unique person to be able to do both so well.

Today I want to talk about the notion of proof, with all its various meanings.

Jennifer and Dana Randall helped create the area that now joins theorists and physicists who work on various Markov type systems. They started with a lone workshop, and now the area is a thriving part of both disciplines. When they started what was a proof in one area was not necessarily one in the other. This, Dana tells me, often led to comments like this being made during one of her presentations:

But Dana that is not an open problem, X “proved” it years ago in ${\dots}$

One of the great achievements of Jennifer and Dana, with help from many others, is to reduce this dissonance about what proof means. Those from theory and those from physics, who work on Markov systems, may still not completely agree on what is a proof, but the differences are at least now acknowledged.

This made me think about what kinds of proofs there are and how they differ.

Types of Proofs—Silly?

${\bullet}$ Proof Reading: Ken and I try hard to proof-read these pieces for typos, math errors, and general examples of poor communication. We try very hard, but we know that we often fail short. One type of activity that has “proof” in it is the art of proof reading. ${ }$ Or is it proofreading? I have noticed that the New York Times almost never has spelling errors these days—thanks to spellcheckers—but grammar errors are another story. Oh well, I guess that’s progress.

${\bullet}$ Proof of Vodka

In the spirit of the holiday season we thought we would mention the notion of “proof” as used in the US to measure the content of alcohol in a beverage. I no longer drink—long story—but still appreciate that many do enjoy wine, beer, or even more adult type beverages. According to our friends at Wikipedia: Alcohol proof in the United States is defined as twice the percentage of alcohol by volume. Consequently, 100-proof whiskey contains 50% alcohol by volume (abv); 86-proof whiskey contains 43% alcohol. The terminology used in the United States is “n” proof, where “n” is a number—not “n” degrees proof.

Why “proof”? The proof that alcohol wasn’t overly watered down was that gunpowder would burn in it rather than be doused by the water. For rum this threshold was measured at 57.15% abv, so that became “100% proof.” The accurate British multiplied abv by 7/4 to get proof for any abv, but the rough Americans multiplied by 2. Now both countries require abv to be stated on bottles, proof being optional.

${\bullet}$ Legal Proof

Perhaps it is best to skip this one, since it is so unclear. What is “proof” in the legal sense seems to be dependent on obvious stuff like country—legal rules differ from place to place. But even within the same country with the same rules, the notion of legal proof seems to depend on time, and perhaps on some hidden random variables. ${ }$ The definition linked to by Wikipedia is a 190-page PDF file with an awkward space in its URL. It defines legal proof as what the laws that define the status quo require in order to change the status quo. So let’s skip it.

${\bullet}$ Proof of Pudding

This is also the season for various treats that are called puddings. I especially like bread puddings of various kinds. The phrase “the proof is in the pudding” is a misquote of a misquixote—something mis-attributed to Miguel de Cervantes, Don Quixote (1615). The form credited to Cervantes is correct but is said by this site to date to the 1300’s and first appear in print in a 1605 work by William Camden: “The proof of the pudding is in the eating.” Here “proof” has its root meaning from Latin proba as “test.”

There also is the Yale University “Proof of the Pudding,” an all-female a cappella group specializing in jazz and swing. As an ex-professor of that great institution I agree that this is another fun use of the notion of proof of the pudding.

Math and Physics—Serious?

${\bullet}$ Math Proof: We could go on for days about what is a math proof. In many of our posts we discuss specific proofs, or we discuss general issues about proof. So I will not spend much time on it now. I do note that there still is a long trail of comments on whether or not the reals are countable or uncountable. So the notion of mathematical proof is not as clear-cut as some would like to believe.

${\bullet}$ Physics Proof The real point today is to return back to Jennifer and Dana examples of the disconnect between mathematical types of proofs and physics type proofs.

The simple point is this: physics accepts as a “proof” things that we would not and do not. Some examples to make the point are in order.

Physics Proofs?

${\bullet }$ An Old Old Example: The Dirichlet Principle, named of course for Lejeune Dirchlet, is the “obvious” notion that certain functions exist that obtain a minimum value. Note we are talking about functions that have some minimum value, not points.

There is a book that is out of print that whose title summaries the issue nicely:

Dirichlet’s principle: A mathematical comedy of errors and its influence on the development of analysis, by Antonie Monna.

The great Bernhard Riemann named the principle after Dirchlet and believed it was obvious, from a physics argument, that there had to always be a solution. Karl Weierstrass later showed that there were reasonable problems of this type without any minimizer—that the principle was false in full generality.

The reason it was thought to be “obvious” was the analogy to calculus. We are probably familiar with the idea of finding the real number ${x}$ so that some given function ${f(x)}$ is minimized for ${x}$ in ${[0,1]}$, for example. A typical calculus problem might be: Find the value ${x}$ so that

$\displaystyle e^{x} - x$

is smallest for ${x}$ in ${[0,1,]}$. This is the one of the prime applications of calculus.

Things get more difficult when we replace ${x}$ by a function ${u(t)}$ and ${f}$ by a functional ${\Phi}$ and ask for the ${u(t)}$ that makes

$\displaystyle \Phi(u(t))$

the smallest possible. An ancient example is to ask for the curve ${u(t)}$ that has length ${1}$ and encloses the most area in the plane: the functional ${\Phi}$ determines the area of the curve ${u(t)}$. This is the famous isoperimetric problem, whose answer is well known to be the circle with circumference ${1}$.

The problem is that it is not hard to guess that the circle is the solution, proving that it is the solution is much harder. Jakob Steiner in 1838, showed that if there was a minimum, then it was the circle. He did this by a very clever argument based on taking any non-circle and making it more symmetric, and making the area not decrease. The difficulty with this argument is the proof that there is a minimum. That is the hard part of the proof—see this for a discussion.

Finally see the following for a silly solution in the spirit of the holidays:

Consider the large class of animals capable of changing their ratio of surface area to volume. (And note that these animals live — approximately — in Euclidean 3-space.) What do these animals do when it’s cold? They curl up into a ball! More precisely, they assume the closest approximation to a ball that they can manage. This is because any exposed surface area is a place where heat is lost, and curling up into a ball minimizes that surface area. So a spherical or “ball” shape keeps animals warmer. Now, here’s how these ideas can be turned into a 4-line “biological proof” of the above proposition.

${\bullet}$ Proof by Physical Impossibility?

Suppose one can prove that ${X \implies}$ the feasible ability to travel back in time and kill one’s grandfather. Is this a proof of ${\neg X}$? A similar and more plausible case is when ${X \implies}$ the ability to transmit information at faster than light speed. A controversial example of such an ${X}$ is discussed here.

Are there theorems in quantum information theory for which it is felt that the “nicest” proof is by “reduction to Einstein” rather than from axioms? We note that this paper by Ulvi Yurtsever implies that the ability to maintain a prediction advantage over quantum sources that are adduced to be genuinely random implies the ability to communicate faster than light. We invite readers to comment on other examples and the formal status of this kind of proof.

Open Problems

What is a proof? Must a proof be checkable by a human being unaided by a computer? Note that we could be talking about a checker for the proof, not the proof itself.

1. December 21, 2011 10:32 am

I’d guess that a proof is a high degree of certainty, that some underlying truth will remain an underlying truth in the future. Different systems will require different degrees of certainty. The law may only run on about 80%, while mathematics needs something a lot closer to 99.999…

What makes it interesting is whether on not, even in formal system, there is some form of underlying absolute truth, that is completely unshakable right up to the end of time. We believe this to be true for most of our mathematics, but how certain are we really?

Paul.

• December 21, 2011 10:45 am

Has Pythagorean theorem 100% degree of certainty? Or the degree is less? May be we have to say 99.(9)?

• December 21, 2011 11:19 am

I guess it all depends on how you interpret the ambiguities.

Knowledge is not necessarily as smooth and uniform as we like to believe it is …

• December 21, 2011 12:15 pm

Paul,
Yes, ok. I would be interested to hear your interpretation.
Thank you.

• December 21, 2011 12:44 pm

My initial comment has a number of ambiguities, the Pythagorean theorem on the other hand, seems to be pretty well-defined in both its geometrical origins and its algebraic representations. Time often uncovers gaps, except when the particulars are being explicitly avoided. Sometimes it just takes a guy (or gal) like Cantor to go where others fear to tread …

2. December 21, 2011 10:37 am

When I read the word “Microsoft”, I just remember “Microsoft Windows”. I think that it is not a good OS, but I am unable to prove it. At the same time Microsoft is unable to prove opposite approval. I think this problem is example of some special sort of proof in computer sci. Today we have no method for proofs of this sort 😉

3. December 21, 2011 10:58 am

“Proofs, Proofs, and Proofs” looks like is the last post of this year. My happy new year 2012 card is related with the proof of the four color theorem,

• December 21, 2011 12:18 pm

Happy New Year!
I do hope the four color theorem will be proved in 2012 ;-)))

• December 21, 2011 1:01 pm

Same feeling for polynomial time algorithm for graph Isomorphism testing.in 2012.

• December 21, 2011 8:10 pm

Thank you 🙂

December 21, 2011 11:09 am

With regard to your last point: there’s a nice recent example of “proof by physical impossibility” in quantum information theory. Graeme Smith and John Smolin have recently given a proof that certain quantum channels must have zero quantum capacity, because otherwise it would be possible to use them to implement the unphysical “transpose” operation. While such a proof could ultimately be understood completely mathematically with no reference to physical systems, the physical interpretation is much more natural.

December 21, 2011 11:58 am

Jennifer Chayes is theorist

should be

Jennifer Chayes is a theorist

6. December 21, 2011 12:53 pm

The natural conjugate to “proof by physical impossibility” is “conjecture by physical possibility”. As an example of the latter, the principle of causal separability is dear to engineers; it requires that our simulations (a) represent measurements as processes that are separably localized in space and time, such that (b) the communication channels associated to separable measurement processes are causal (that is, their channel capacity is zero for processes that are backwards-in-time and/or outside of relativistic light-cones).

Broadly speaking, at present mathematicians and scientists know how to represent causally separable dynamical processes in only two ways: (1) on Hilbert state-spaces as Kraus operators, and (2) on rank-1 tensor product spaces, i.e. classical state-spaces. In the former case causal separability arises via dynamics that is locally Hamiltonian and globally unitary, as described by algebraic theorems due to Choi and Kraus (and many others); these powerful theorems are of course the foundations of modern quantum information theory. In the latter case causal separability is built-in to various (nontrivial) classical state-space geometries; in general the associated dynamical flow need not be Hamiltonian although in practice it usually is — the Chaplygin Sleigh is an example of non-Hamiltonian classical dynamics.

We can “conjecture by physical possibility” that options (1) and (2) are neither exhaustive nor exclusive, but rather represent two extremes of a continuum of causally separable dynamical theories. One physical possibility that points toward this conjecture is that the simulation codes in common use represent dynamical state-spaces whose geometry is more-than-classical yet less-than-Hilbert, and these hybrid state-spaces are (in practice) remarkably successful at describing Nature. At present we do not commonly use these codes to simulate channel capacities, yet even if we did, minor causality/separability violations would be masked by the noise that is ubiquitously present in realistic simulations. And perhaps this masking is a clue? Perhaps within the context of causal separability, noise assumes a more fundamental role than “Schmutzphysik” (as Pauli famously called it)?

December 21, 2011 1:40 pm

We might think of physics ‘proofs’ as a category mistake. Often they are merely concerned with making falsifiable claims and then running said claims through a gauntlet to gain a sort of confidence of corroboration and usefulness (a la Popper). I think the gut instinct in physics (helped more by science reporting and fleeting feelings left by modernism and empiricism before it) is to claim a sort of universality and highly weighted metaphysical importance to this corroboration (all physicists I know don’t do this; usually they are more concerned with the solving of physics problems than assigning them great meaning). From all of this is born the physics proof – which is usually more of an informed intuition on what testable implications certain claims may have and how these probable implications relate to other established corroborations. I think physics proofs are often taken too far and used too freely.

Now math proofs. Ideal math proofs are certanties. But these are certainties of a different sort. What sort of certainties are they? Ignoring man’s fallibility and other imperfections in actual practiced mathematics, ideal math proofs entail just one certainty: if you believe this list of axioms (A, B, C) and these rules of inference (A -> B, !B -> !A) etc, then you also ought to believe this statement, and here is why. Namely, ideal math proofs show with certainty that statements follow from other statements (a la Mathematical Formalism). Something different happens when we wish to apply our statements and symbols in the world. And ultimately, these math proofs are an ideal we strive towards; not something we have.

Both proof varieties have different utility and different domains of applicability. I think going forward we need to be clear to ourselves about what sort of proof methodology we are using, and to think and check with others whether our methodology is a useful way to approach our problems.

December 21, 2011 2:16 pm

The BEST paper I ever read about how Mathematical Theorems get accepted
by the community was

Social Processes and Proofs of Theorems and Programs.
by De Millo, Lipton, and Perlis.

December 21, 2011 6:18 pm

> Must a proof be checkable by a human being unaided by a computer?

A proof doesn’t have to be understandable by a human brain – it must only be valid. The four-color theorem has been proved by several programs including the Coq proof-checker, whereas Fermat’s last theorem has been amply checked by the mathematics community. For me, both processes are equally worthy of trust.

• December 21, 2011 7:01 pm

Wouldn’t be better to say “Now I can understand and it is valid”?

December 21, 2011 7:35 pm

Yes, of course this is better whenever it’s achievable, and these are the only kinds of proofs we’re taught at school. But there are also a few monsters: proofs which only a few humans can understand… and proofs which only a computer can understand.

• December 22, 2011 7:48 am

To Serge’s list of mathematical “monsters”

“proofs which only a few humans can understand … and proofs which only a computer can understand … “

surely we can add another natural class of mathematical monsters

” … and theorems whose preconditions only oracles can verify.”

Hmmm … what other varieties of mathematical monsters are extant?

Like most folks, I think it best that no attempts be made to abolish monsters from mathematics. To the contrary, mathematics is wonderfully fearsome and awe-inspiring precisely because “here there be monsters.”

December 22, 2011 1:13 pm

The classification of finite simple groups: several thousands of pages. Specialists are still trying to reduce the length of the proof. It’s the same phenomenon as for the 4-color theorem, where they try to reduce the number of cases tested by the computer. One may wonder if the complexity of a proof is inherent in the theorem itself. However I never believed that Fermat had actually found a “wonderful proof” of his theorem… 🙂

10. December 21, 2011 10:45 pm

Since CS has only one standard of proof I remember being surprised by the distinction between “theoretical physics” and “mathematical physics”. The kind of physics that Jennifer does is mathematical, where the proofs meet the math standard, versus theoretical, where the “proofs” are often based on incredibly strong assumptions (the usual term for such an assumption is an “Ansatz”) that sometimes are clearly false or even based on operations that violate mathematical rules. Under these assumptions, one can produce “exact” answers to physical problems, so people can “know” what these solutions are theoretically without having ever proved it. I recall Jennifer commenting that many theoretical physicists would see some mathematical physics paper that actually proved the value of some quantity without using an Ansatz and claim “but we already knew that”.

For example, one might analyze 3CNF formulas using a “mean field” assumption about the variable-clause incidence graph and derive some bound based on this assumption, even though almost no individual formulas have this property. However, there are other cases where the mathematics itself sounds bizarre: Compute some property of the Hamiltonian of some system that consists of replicas of some fixed system, deriving some formula Z(n) for the case with n copies and take the derivative of the limit of log Z(n) as n – now a continuous parameter – approaches 0.

Maybe the closest analogy in TCS is in cryptography where proofs are all reductions. Nobody is proving absolute security. (Which can get Neal Koblitz upset about the usof the term.) However The physics “proofs” I have seen are often implicit reductions to many different Ansatzes.in the same argument and some of these are as strange or stranger than the kind of thing I mentioned above. On the other hand, there is often is a strong intuition people have in using these Ansatzes that we don’t necessarily get from our legalistic proof standards.

• December 24, 2011 7:39 am

One thing to watch out for when reading physics papers, or books, is the distinction between “exact” and “rigorous” results. The “exact” results are, by the author at least, expected to give the correct answer to a precise mathematical question, but the derivation of that answer may contain lots of hidden assumptions and steps which can’t be justified mathematically. The “rigorous” results on the other claim to be based on proper mathematical proofs without hidden assumptions.

December 22, 2011 9:50 am

Thomson problem on repulsive points on the sphere (http://en.wikipedia.org/wiki/Thomson_problem) provides, in my opinion, an interesting example of the “proof by an experiment” (or “proof by physical realization”) especially for the case with small number of points, e.g. five. As noticed in the above Wiki page the first rigorous computer assisted proof was announced only in 2010 in http://arxiv.org/abs/1001.3702

December 23, 2011 9:38 am

Passionate post!

“Must a proof be checkable by a human being unaided by a computer?”

To set and carry out an experience on elementary particles, physicists can’t avoid to use tools to operate on these objects. In Mathematics too, there are monstrous computational processes or proofs only computers can carry out.
So, to your question, i say definitely: no!

Merry Christmas to all!

13. January 2, 2012 2:50 pm

In (mathematical) logics, a proof is an actual, well-defined object. Mathematics should work in the same way, but rigor is lost because we humans need shortcuts lest we lose overview.