Designing a proof with a tablet

The other day I was working with colleagues on the analysis of a streaming algorithm. We got to the stage where it seemed plausible that we had gathered all the ideas needed to analyze that algorithm - or maybe some variant, if necessary - using a hierarchy of cases with some predicates that we had roughly outlined - or maybe some variant if our study was incomplete. I had the impression that we might have had all the ideas that were necessary to build a proof, but things were hazy in my mind. I thought there was a proof lurking in there, waiting to be revealed, but I was not sure of it. It was as if we were trying to bake a cake, had gathered what we hoped was a sufficient collection of ingredients and utensils, and the only work that remained was to mix and bake them the right way.

At that point, what is required is no longer brain-storming but a more careful, structured attempt to execute a proof, and in my experience at that stage it is more efficient to work alone. I decided to give it a go. But, after two hours editing a Latex file (that already contained some proof of a related but weaker result), I gave up in frustration. The distraction of text editing and the inability to have at hand the shifting pictures that had been trying to form in my mind, prevented me from making any progress. I kept losing track of where I was headed, and was becoming less confident that there wasn't a major hole somewhere. Working with the file was just a waste of time.

Then I picked up my tablet and stylus, and gave it another try.

I slowly went through a proof attempt, drawing small sketches, writing definitions and calculations next to them. For my figures, there were as many colors available as I wished. When I made a mistake, erasing and modifying was easy and did not create a mess, as it would have if I had been working on paper. When I had to consider several similar cases, I could copy-paste the same figure several times, instead of having to redraw it, as I would have had to if I had been working on the white board. With no such side concerns to distract me, I was able to focus exclusively on the Ariane thread of my reasoning, and brought the rough proof to what I thought was a successful conclusion after filling a dozen tablet slides. On the last slide, using copy-paste, I gathered all the inequalities scattered throughout the text, then stared at them and verified that the proof was complete. At that point, I knew I had a proof. But nobody else would have been able to tell, because of various inconsistencies that only I would know were minor. In fact, even myself, if I had let it sit and had waited a few days before picking it up again, would then have been puzzled, would have wondered whether I really did have a valid proof, and would then have had to work through it again, wasting time by a needless repetition of side trips into dead end reasonings.

So I went through the proof again to clean it up: between the first and the last slide, notations had evolved, and some separations into sub-cases had turned out to be unnecessary. I went through it slowly, going back and forth to check notations, conditions, and to ensure consistency. Along the way, I underlined the main steps in the calculation - now that I had done it once, I knew better which ones were important in the end. With the fresh knowledge of how they fit together in the final wrap-up argument, I re-ordered them so that they were proved, as much as possible, in the order in which they would be needed in the end -- checking, as I was doing that, that that re-organization did not conflict with the timing of the definitions and notations.

I was pleased with the final result on the tablet. All I had to do was quickly type a Latex version of the slides (omitting the figures, that are too much work to do), which turned out to be about a page long, and I was done.

In just a few hours, I had gone from a collection of slightly fuzzy ideas to a proof that was maybe not yet a model of readability, but that was complete, structured, and coherent - in other words, a proof that, for a patient reader, was verifiable. I could now claim the result.

Without a tablet, I don't think that I could have done it so fast. With the tablet, everything that I try to picture in my mind can be laid down immediately. I am free to focus exclusively on the mathematical reasoning, without any unwelcome distractions: there is no technological barrier. It is for such reasons that I am a big fan of tablets with pen input.