Casual tours around proofs

Question

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 fit 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 big-list, with the hope that it will actually be.

Answer 1

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

Answer 2

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.

Answer 3

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

Answer 4

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

Answer 5

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.