# Casual tours around proofs

Today Ryan Williams posted an article on the arXiv (previously appeared in SIGACT News) containing a less technical version of his recent ACC lower bound technique.

My question is not about the technique itself (of course worthy of immense praise), but it's about the style of the paper. In the abstract, he writes:

The proof will be described from the perspective of someone trying to discover it.

Awesome! In the Background section he adds:

This article is a discussion about how to discover the proof – a casual tour around it. Not all details will be given, but you will see where all the pieces came from, and how they ﬁt together. The path will be littered with my own biased intuitions about complexity theory – what I think should and shouldn’t be true, and why. Much of this intuition may well be wrong; however I can say it has led me in a productive direction on at least one occasion.

This is amazing and it's the first time that I have seen it. I have always wondered why authors of paper don't write how they got to the proof, including the failed approaches they tried before getting to the track that led the solution. When I saw Ryan's paper on the arXiv, I felt very motivated to read it. I consider it a revolutionary paper from this point of view. Most of the time the only thing you can do with a paper is verifying its correctness.

The question is the following:

• are you aware of other papers in TCS where a breakthrough result is presented in a "casual tour" rather than a series of technical lemmas?

I am talking about publications in journals, not blog posts or technical reports.

Also, I tagged it as , with the hope that it will actually be.

-
As a side point, I had an email exchange with Ryan today about writing a post about this paper for the CSTheory Community Blog. My current plan is to write it sometime next week. However, Alessandro, if you are motivated by the paper and would like to do so, please do let me know. :-) –  Aaron Sterling Nov 8 '11 at 23:29
I know you don't want blog posts, but Andrew Drucker's plausible reconstruction of the discovery process behind Valiant-Vazirani theorem is really nice: andysresearch.blogspot.com/2007/06/… –  Diego de Estrada Nov 9 '11 at 0:21
Great question, Alessandro! –  Michal Kotowski Nov 9 '11 at 4:34
For expository articles, see also this MO question: Which journals publish expository work? –  Kaveh Nov 9 '11 at 16:15
Also, I had an email exchange with @AaronSterling and we agreed that I am going to write the blog post during the Christmas break. –  Alessandro Cosentino Nov 11 '11 at 13:56

There is a paper (2001) of similar style by Lov Grover, which describes the way to his breakthrough quantum search algorithm (1996).

-
nice! I was hoping to see an example from QC. –  Alessandro Cosentino Nov 9 '11 at 0:09

Tim Gowers is a fan of this kind of thing. See specifically his exposition of Razborov's method of approximations.

In his introduction, Gowers references my expository article on forcing, which is a (not entirely successful) attempt to do the same thing for forcing. Forcing is normally thought of as a technique in logic and set theory, but it has found its way into TCS occasionally. It comes up in the study of bounded arithmetic and propositional proof complexity (Krajíček and Takeuti are two researchers who have pursued this connection), and the concept of a generic oracle is related to the concept of a generic filter.

-

(This started out as a comment and got way way way too long).

You may enjoy William Thurston's article On Proof and Progress in Mathematics.

Mathematics in some sense has a common language: a language of symbols, technical definitions, computations, and logic. This language efficiently conveys some, but not all, modes of mathematical thinking. Mathematicians learn to translate certain things almost unconsciously from one mental mode to the other, so that some statements quickly become clear. [...]

People familiar with ways of doing things in a subfield recognize various patterns of statements or formulas as idioms or circumlocution for certain concepts or mental images. But to people not already familiar with what’s going on the same patterns are not very illuminating; they are often even misleading. The language is not alive except to those who use it. [...]

We mathematicians need to put far greater effort into communicating mathematical ideas. To accomplish this, we need to pay much more attention to communicating not just our definitions, theorems, and proofs, but also our ways of thinking. We need to appreciate the value of different ways of thinking about the same mathematical structure. We need to focus far more energy on understanding and explaining the basic mental infrastructure of mathematics—with consequently less energy on the most recent results. This entails developing mathematical language that is effective for the radical purpose of conveying ideas to people who don’t already know them.

Regarding the original question, there are papers that do not present ideas in the Definition-Theorem-Proof (DTP) format. Timothy Chow has a few papers that focus on communicating ideas (though they are not the first (or second) papers on the topic/result).

1. You could have invented spectral sequences, Timothy Chow, Notices of the AMS
2. Forcing for dummies, Timothy Chow

One possible reason for the prevalence of the DTP format is that we are all just used to it from books and papers. Reviewers (and readers) sometimes find non-standard writing style distracting. A middle ground is papers that gently break the reader into a result. There are papers that present a special case or a simple problem that illustrates the general idea.

1. The Topological Structure of Asynchronous Computability, Maurice Herlihy and Nir Shavit. The paper has many illustrations and demonstrates the general idea for a simple protocol before applying the main theorem to solve some open problems.
2. Logic and $p$ recognizable sets of integers, Véronique Bruyàre, Georges Hansel, Christian Michaux, and Roger Villemaire. A survey-style exposition of a beautiful result: the sets of natural numbers that are encodable by finite automata, independent of the base chosen are precisely those definable in Presburger arithmetic. The paper has numerous examples, covers special cases before the general case and provides historical background about erroneous proof attempts.

No discussion of a non-standard presentation of remarkable ideas would be complete without mentioning the work of Jean-Yves Girard. Unique is probably the best word to describe it (without being diplomatic or sarcastic). From, the paper Linear Logic.

The philosophical exegesis of Heyting’s rules leaves in fact very little room for a further discussion of the intuitionistic calculus; but has anybody ever seriously tried? In fact, linear logic, which is a clear and clean extension of usual logic, can be reached through a more perspicuous analysis of the semantics of proofs (not very far from the computer-science approach and thus relegated to the next section), or by certain more or less immediate considerations about sequent calculus. These considerations are of immediate geometrical meaning, but in order to understand them, one has to forget the intentions, remembering, with a Chinese leader, that it’s not the colour of the cat that matters, but the fact that it catches mice.

Later:

There are still people saying that , in order to make computer science, one essentially needs a soldering iron; this opinion is shared by logicians who despise computer science and by engineers who despise theoreticians. However, in recent years, the need for a logical study of programmation has become clearer and clearer and the linkage logic-computer-science seems irreversible. [...]
In some sense , logic plays the same role as the one played by geometry w.r.t. physics: the geometrical frame imposes certain conservation results, for instance, the Stokes formula. The symmetries of logic presumably express deep conservation of information, in form which have not yet been rightly conceptualised.

-
Another point is that the DTP style is a common baseline. No matter how you think about the intuition to a problem, there's an "objective" DTP version of a proof. However, intuition itself is very subjective, and my explanation of how I think about a problem might not work for someone else, especially for deep results that admit many interpretations. –  Suresh Venkat Nov 9 '11 at 16:43
"...in recent years, the need for a logical study of programmation has become clearer and clearer and the linkage logic-computer-science seems irreversible..." dewey.info/class/00/about.en 000 Computer science, information & general works 000 Computer science, knowledge & systems Not a coincidence. –  Kris Nov 11 '11 at 7:54

Maybe authors don't include these failed attempts and the story of the research in their published papers because of the constraints imposed by editors and PC members. I guess it is very unusual for a journal (and probably even more unusual for a conference) to accept a paper where the main part of it is devoted to failed attempts. But in most cases if you talk with the authors or experts in the area they will explain story and the failed attempts (and many do talk about these in workshops).

I have seen several authors explain at lease where the ideas came from in their papers. As an example, Girard explains in his paper that the idea for linear logic came from trying to find a denotational semantics for intuitionistic OR. You can find this kind of information also in monographs and biographies of famous researchers and volumes devoted to them (Halmos's autobiography and more recent "Kreiseliana: About and Around Georg Kreisel" edited by Odifreddi came to mind, there are also volumes and articles dedicated to some complexity theorists). Hopefully more people will do what Ryan have done and systematically explain the process and tell the story.

ps: you can think of these as oral tradition of research :) (somewhat similar to Oral Torah which was not allowed to be written down).

-
thanks for the answer, although I wanted to avoid this kind of answers. I intentionally didn't ask for the reasons why this doesn't happen often. Also, note that I pointed to Ryan's result, because it's a "normal" paper, not a blog post, or a textbook or a biography. –  Alessandro Cosentino Nov 9 '11 at 1:17
@Alessandro, but you didn't avoid it: "I have always wondered why authors of paper don't write how they got to the proof, including the failed approaches they tried before getting to the track that led the solution." They do it, but usually not in journal papers (I think this kind of information is mainly interesting for junior researchers and students working in that particular topic). But I agree with you that reading papers which tell a story is more enjoyable. A few senior researchers advised me to do that, also in talks and presentations. –  Kaveh Nov 9 '11 at 1:39
There might be also other reasons that why including such information in journal articles would not be well-perceived by senior researchers (I have heard criticism from mathematicians about papers in TCS, they say that when reading TCS papers it feels like we are over-advertising our results, it seems that they like it the other way more). (By the way, correct me if I am wrong but I think Ryan's article is not published yet.) –  Kaveh Nov 9 '11 at 1:45
Sanjeev Arora once said in a talk that he started out trying to prove PCP hardness for Euclidean TSP, and the failure to do so led him to a PTAS. –  Suresh Venkat Nov 9 '11 at 6:46
I've found that readers are often happier when I leave out the failures, because keeping track of which techniques are important and which are red herrings adds an additional layer of difficulty to reading the paper. It's harder, but better, to find an intuitive story which leads directly to the correct solution --- even if you didn't think up the story until after you found the proof. –  Neel Krishnaswami Nov 9 '11 at 6:55

There is a published paper by Laszlo Babai (1990) in the form of a fable about Arthur and Merlin describing the dramatic sequence of events leading the community up to the IP=PSPACE result in 1989, which was very much unbelievable just a year earlier.

-