Reading Messy Proofs

In fall of 1985 when I started graduate school, my advisor Michael Sipser asked me to read an early handwritten manuscript by Johan Håstad of his switching lemma. I spent many hours decoding the notation and working through the messy conditional probabilities until I felt I had checked every step of the proof. When I started presenting this to Sipser, he stopped me and said he didn't want the details but instead the intuition of the proof. I had nothing.

I'm reminded of this story as I hear the complaints of how badly OpenAI wrote the 712 papers released on October 6th, as though humans wrote crystal-clear proofs beforehand, definitely not the case in general, especially in the early versions.

Noam Nisan once told me that reading a badly written proof leads to better understanding since you really need to figure out the details instead of having them neatly spelled out. Perhaps, but do not use this as an excuse for not taking the time to write the details properly.

I approach reading the proof of a new result by assuming the proof is wrong until I'm convinced otherwise. Working my way through early versions of Immerman-Szelepcsényi and Toda's theorem definitely forced me to understand these proofs well so I could explain them to others.

I just gave up on fully understanding some results like the original PCP theorem and Ran Raz's Parallel Repetition Theorem, despite seeing the authors give talks on the papers. Sometimes you have to trust the authors and others who hopefully have read the paper. Don't even get me started on László Babai's Graph Isomorphism in quasipolynomial time. And some papers, like Primes in P, require mathematical results in other subfields that I just have to accept.

Sometimes you'll just get better versions of proofs, most famously Irit Dinur's combinatorial proof of the PCP theorem. I only really understood the switching lemma years later when Sophie Laplante and I wrote a Kolmogorov complexity-based proof building on a then-new proof of Alexander Razborov.

When I get stuck in a proof, I sometimes ask the authors, but usually as a last resort unless I can talk to them in person. That's an advantage we have now: you can ask AI to get you over a hurdle in a proof. Claude, while maybe not as good at proving theorems as the unreleased OpenAI model, does a better job writing them up. And one hopes that we'll see simplified and possibly strengthened versions of some of these important results, written by humans or human-AI collaborations. Maybe we'll even get the intuition Sipser told me to seek all those years ago.