Characterizing visual proofs

Question

``Proofs without words'' is a popular column in the Mathematics magazine.

Question: What would be a nice way to characterize which assertions have such visual proofs? What definitions would one need?

I suspect that in order to make this question precise, one will have to define a computational model for the ``visual verifier'' and postulate the possibility of a visual proof if there is a quick verification algorithm, and the visual proof itself is short.

Rev. 1:

To elaborate: the intriguing and essential feature of a visual proof is that the proof can be ``read'' or verified rather quickly using primitive operations that are different than those involved in reading and verifying textual proofs (e.g., area comparison or counting). These are operations that are native and quick for the visual system. (There may be other operations that could be used as well: color, texture, shape, or any other visual cue could be part of the repertoire.) It is not necessary that for an assertion to have a visual proof, that it involve inequalities, though this feature does lend itself relatively easily to a direct visual proof.

Thus, one could frame the notion of a visual proof as follows: An assertion has a visual proof if there is a map from the space of assertions (strings over an alphabet) to the space of pictures (strings over a visual alphabet) such that assuming a particular computational model of a visual verifier, there is an algorithm for reading the visual proof that is faster than the best one for reading the textual proof.

The computational model of the verifier allows one to specify what visual primitives may be used and how ``costly'' they are in the algorithm. (For example, if a proof is mapped to a picture that only uses length of a line to represent elements in the proof, then reading the proof will likely be slow, whereas if it uses length and area, the proof might be immediately verified.)

This leads to a sort of complexity theory of visualizations. In fact, it implies that visualization is a special case of a more general activity: re-encoding a given problem so that one can exploit a fast algorithm.

There may be some assertions that have no maps that can be verified quicker than the original proof. What might these be?

I hope this provides a better context for my question.

Thank you for your comments in advance. I appreciate your attention and intellectual work.

Answer 1

Here is a complexity theory perspective. Be warned that it may differ wildly from someone whose primary focus is logic.

I think the appropriate definition of a "visual proof" would boil down to giving an appropriate definition of what a verifier does with such a proof. Proof systems in complexity theory are measured by (a) how much the prover and verifier "interact", (b) the allowed lengths of potential proofs, and (c) the power of the verifier.

In the framework you are proposing, the prover simply gives the verifier a proof and walks away. So (a) is already determined. Also, the visual proof is presumably written on a small sheet of paper, so (b) is essentially determined (let's say the visual proof can be encoded in length that is at most a fixed polynomial in the length of the claim).

That leaves (c), which is where proof complexity gets interesting. It turns out that verifiers can be surprisingly weak and still verify the proof of any statement which has short proofs (where "short" is "fixed polynomial"). For example, if you require that proofs be written on a two-dimensional grid, then for every theorem with short proofs, there are proofs of the theorem which can be verified by a two-dimensional finite automaton, see

J. Hartmanis, D. Ranjan R. Chang, and P. Rohatyi. On IP = PSPACE and theorems with narrow proofs. EATCS-Bulletin, 41:166–174, 1990.

A verifier could be a "streaming" algorithm: it could be randomized, go over the proof in just one pass, and use a tiny amount of workspace relative to the length of the proof, see

Richard J. Lipton: Efficient Checking of Computations. STACS 1990: 207-215

The famous PCP theorem (of Arora et al.) tells us that the verifier could even be a "spot checker" which is randomized and only probes the proof at a constant number of points (which depend on the random coin tosses).

All of these are effectively different ways of characterizing the class NP: the polynomial time verifier in the definition of NP can be replaced with verifiers of the above kind.

So I believe that a good characterization of "visual proof" would turn out to give yet another way in which a simple verifier can check the proof of a theorem. However it is natural to think that maybe not all theorems with short proofs should have short visual proofs, so perhaps it is too ambitious to think that all of NP should have "visual proofs". Hence your definition problem will be a delicate combination of figuring out what the verifier should be able to do in a visual proof, and what kinds of true statements should admit such proofs. Good luck!

Addendum (added 7/1/10). The following neat paper on "Approximate Testing of Visual Properties" (doi: 10.1007/978-3-540-45198-3_31) by Sofya Raskhodnikova looks very relevant: http://people.csail.mit.edu/sofya/pixels.pdf

Answer 2

Question: What would be a nice way to characterize which assertions have such visual proofs? What definitions would one need?

I am not sure if this helps but you might want to check out Visualizing Inequalities by Alsina and Nelsen. Roger Nelsen is also the author of two other books (Proofs without Words) which is a collection of many of those columns in the Mathematics magazine.

Coming back to the book, it gives no definite characterization of visual proofs but it does list various methods by which inequalities can be represented through geometric figures. It provides the beginnings of a "Representation theory for inequalities " (!) if you may call it that.

It discusses how the circumcircle and the in-circle (Chapter 4) can be used to represent an inequality between the radius of circle and the length, perimeter or area of n-gons. This doesn't always work for n-gons with n > 3 since they may not have both the circumcircle and the in-circle.

To visually prove geometric inequalities, one can use isometric transformations such as reflection or rotation (Chap 5 and 6). One can also use non-isometric transformations (Chap 7) such as

1. Similarity of figures which preserve shape but change measure
2. Measure-preserving transformations which change shape
3. Projections which change shape.

I particularly liked Figures 1.4, 1.7, 1.14, 1.17, 2.6, 2.17, 4.4, 7.8, 7.9, 8.17, 8.18, 8.20.

one will have to define a computational model for the ``visual verifier''

Regarding this part of the question, there is prior work on Geometric Theorem Proving. (Is that what you meant?) A couple of books which come to mind are Mechanical Geometry Theorem Proving by Chou and Wu's Mathematics Mechanization. Also see the GEO-Prover

Some relevant papers are

1. Kapur, D. 1986. Using Grobner bases to reason about geometry problems. J. Symb. Comput. 2, 4 (Dec. 1986), 399-408. DOI= https://doi.org/10.1006/jsco.1995.1056
2. Kutzler, B. and Stifter, S. 1986. On the application of Buchberger's algorithm to automated geometry theorem proving. J. Symb. Comput. 2, 4 (Dec. 1986), 389-397.’
3. Kutzler Stifter Automated geometry theorem proving using Buchberger's algorithm https://dl.acm.org/doi/10.1145/32439.32480

Answer 3

This may not directly answer to your question. A different MO question about Resources for graphical languages accumulated quite a few references for proofs based on string diagrams. These have precise semantics generally in terms of monoidal categories and can be used to prove results about quantum groups among other things.

Answer 4

I realize that it is a bit tangential to the intent of your question, but it seems to me that it bears mentioning here the widely acclaimed work of Edward Tufte, in particular, his two books, “Visual Explanations”, and “The Visual Display of Quantitative Information”.

Answer 5

Here are a couple of examples to keep in mind when considering such visual proof systems.

First, one can use variations on the Todd-Coxeter coset enumeration algorithm to yield Schreier coset graphs which yield visual proofs of identities for groups presented by generators and relations. Here one fits the relators together like pieces of a puzzle. I recall I once did that for an exercise in a knot theory seminar and it was one of the few times I saw George Whitehead smile! I wish I could remember the specific example.

See also Mark Haiman's Proof theory for linear lattices which transforms graphs rather than formulas, e.g. see below for such a proof of Desargues implication and its dual from Fig. 4 p. 226.