Bad news: The Turing award winner and father of LaTeX thinks the proofs you (and everyone else) are writing are sloppy, non-rigorous and quite likely flat-out wrong. But there’s good news too: Sir Michael Atiyah is not quite so sure.

In one of the more combative talks at this year’s HLF, on Tuesday morning Lamport outlined his issues with the current state of proofs in mathematics, and gave us a glimpse of his preferred system. Essentially, while much about maths notation has moved on since the 17th century, he thinks the prevalent style of writing proofs has not, and that it’s over-reliant on prose, wilfully terse, and fatally prone to obscuring errors. For Lamport, the purpose of a proof is to make sure that the result you’re trying to prove is actually true, and current proofs are simply not fit for this purpose.

I’m sure anyone who’s waded through a typical published proof, trying in desperation to tie together the unexplained inferences, can sympathise. If you do, then Lamport’s half-hour talk How to Write a 21st Century Proof is well worth a watch. (He also has a paper explaining the same ideas.) He reworks a proof from Spivak’s Calculus of a corollary to the Mean Value Theorem, and his hierarchical structure and thorough referencing of the justifications for each step certainly seemed like they’d be appreciated by a reader new to the result. He imagines a possible future of proofs in hypertext, with collapsible layers of explanation, optional sketches and other extras to help guide you through a dense proof.

But Lamport’s ideas haven’t been met with universal agreement at the HLF. When he asked rhetorically whether a student should be expected to hunt through a textbook to find a statement 36 pages earlier justifying a step of the proof, I thought I heard a muttered “Yes!” from the audience.

Sir Michael Atiyah was not wholly convinced either. During his press conference later in the day, the Fields medalist said in passing that he had agreed with 90% of Lamport’s talk, and disagreed with 90% of it.

Later in the conference, I asked Atiyah about his recent work on the Feit-Thompson Theorem (a result from my area of maths, finite group theory). He has a proposed new proof, an order of magnitude shorter than the current 255-page behemoth. He took the opportunity of my question to return to his thoughts on proofs, jokingly saying in reference to the 12-page one he was carrying a copy of, “If you want to know how to write a proof for the twenty-first century […] this is it!”

Atiyah likened his view of a theorem to a building with foundations and inner structure, rather than a chain in which each link is crucial to prevent the whole thing falling apart. “A good theorem has structural stability”, and if you really understand a proof, a hole in one window will not cause the whole edifice to collapse.

Perhaps both ways of looking at these things are necessary. Understanding the high-level structure behind a theorem is bound to be necessary to place the result in its context and learn about the wider field. But one wonders how many erroneous results are published by authors who thought that they understood the grand structure of their ‘proof’: according to Lamport’s talk, anecdotal evidence suggests one-third of published papers are contain incorrect results. Checking the nitty-gritty details will always be necessary, and as long as published proofs exist that help with neither of these very successfully, advances in either area are to be welcomed.