Leslie Lamport thinks your proofs are bad

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.

Leslie Lamport at the HLF 2017

© Heidelberg Laureate Forum Foundation / Flemming – 2017

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.

Posted by

is a mathematician from Manchester, UK. He worked at The University of Manchester researching finite group theory until 2012. He now works as a data analyst, is an occasional cryptic crossword setter and blogs about maths at The Aperiodical.

2 comments Write a comment

  1. Yes, many proofs need “updates” in order to hold. And there seems to be an increasing number of mathematicians who want to improve the art of proof. Voedvodsky, also a Heidelberg Laureate, even thinks there are better foundations for proofs then set theory.

    Voevodsky at some point radically changed the direction of his research, with one motivation being his growing concern about the increasing danger of mistakes in mathematical proofs. He had personal experience of this in his own work….
    He sees the answer to this problem in the use of computers as “proof assistants”, checking the validity of the arguments of a proof. Though, to develop an effective proof assistant, he found it necessary to think deeply about the foundations of mathematics, which led to the development of what he calls “Univalent Foundations”.

Leave a Reply

E-Mail-Benachrichtigung bei weiteren Kommentaren.
-- Auch möglich: Abo ohne Kommentar. +