Against: the evidence against, the controversies, the failed tests

This file lists the evidence against structured proofs and the definition-theorem-proof style, and where the field disagrees.

1. Structured proofs do not always improve comprehension

Evidence Source Grade
Structured readers were better only at picking a summary; on justifications, transfer and examples they did somewhat worse, mostly not significantly Fuller 2014 measured, one study
In interviews, many students said structured proofs "jumped around" and forced them to scan for related parts Fuller 2014 measured, qualitative
Lamport reports mixed reactions: checkers liked the format, readers who wanted to skim did not Lamport 1995 supported with caveat (author's report)
Lamport concedes the format does not serve a reader who wants the ideas without the details Lamport 1995 supported with caveat
A referee found Lamport's long structured proofs tedious and asked for informal sketches of the key ideas Lamport 2012 supported with caveat (one referee)
Leron's format, in Lamport's view, is no better than prose at avoiding errors Lamport 1995 convention, untested

The only randomised test of a structured layout is Fuller 2014, and it tested Leron's format, not Lamport's.

2. More support in the text can backfire

Evidence Source Grade
Narrated, animated e-Proofs gave no immediate gain and lower retention two weeks later Roy 2017b measured
Eye tracking suggested e-Proof readers made less effort when the narration stopped Roy 2017b measured
Students liked e-Proofs and generic proofs; neither raised comprehension Alcock 2015, Lew 2020 measured

Student preference is therefore not evidence that a format works.

3. The cost of formality

Cost Source Grade
Structured proofs are longer, mainly because they carry more detail Lamport 1995 supported with caveat
Machine-checked proofs are, for now, much harder to write than careful informal ones Lamport 2012 supported with caveat
To an expert the formal setup is often redundant: the reader reconstructs the idea and skips the rest Thurston 1994 supported with caveat
Formal correctness at the scale of whole fields is impractical, and reliability comes from people thinking carefully Thurston 1994 supported with caveat
Proofs are accepted through a social process that formal verification does not reproduce De Millo 1979 convention, untested
The school two-column format made proof a routine and cost students' part in finding the ideas Herbst 2002 supported with caveat (historical analysis)
One of Halmos's advisers found long chains of elaborately stated lemmas boring Halmos 1970 convention, untested

4. The DTP style as hiding intuition

  • Thurston 1994 argues the DTP picture leaves out where questions come from and how understanding moves between people.
  • Thurston 1994 observes that communication narrows from conversation to talk to paper, and the paper keeps the least.
  • Hanna 1990 asks for proofs that explain, not only proofs that prove.
  • Weber 2004 documents a real-analysis course taught as a sequence of definitions, theorems and proofs (secondary).
  • Lamport 2012 replies that prose proofs do not explain either, and that a sketch placed before each level explains better than prose woven into the proof.

5. Where the field disagrees

Disagreement Sides Grade
What a proof is for Leron 1983: communication; Lamport 1995: rigor; Lamport 2012: separate the two goals convention, untested
Whether a given proof is valid 109 mathematicians split on one calculus proof; applied mathematicians accepted it more often measured (Inglis 2013b)
Whether experts skim first Inglis 2012 found no initial skim; Weber 2013 reanalysed and found skimming; Inglis 2013a replied contested
Whether series of lemmas help Halmos's advisers contradicted each other convention, untested
Where notation goes Introduction, separate section, or along the way; no standard place in 22 articles measured, descriptive (Kuteeva 2015)
How an article ends 11 of 22 have no conclusion; some end with QED, some with open questions measured, descriptive (Kuteeva 2015)
Postponing proofs An answer on Ilmavirta 2015 puts precise statements in the introduction; another postpones proofs in long papers and says circularity is easy to check convention, untested
Labelled steps in prose MathOverflow 2021 (example only): unlabelled induction is normal in papers; Lamport 1995 numbers every step convention, untested
Labelling speculation Jaffe 1993 proposed it; Thurston 1994 answered that it misdescribes how mathematics progresses convention, untested

6. Limits of the evidence itself

  • Every comprehension experiment found uses undergraduates, not research mathematicians reading papers.
  • Samples are small: Roy 2017b had 49 students (21 and 28); Fuller 2014's size was not read.
  • Fuller 2014 has no replication that we found.
  • The self-explanation studies (Hodds 2014) come from one team, though across lab and classroom.
  • The genre corpora (Graves 2013, Kuteeva 2015) are 30 and 22 articles.
  • The grey sources are mostly single mathematicians' opinions; four of 23 scored below 10 of 20 (sources.md), and none reports data.
  • Krantz 2017 says his article scheme may not fit papers that fill a whole journal issue, such as the Feit-Thompson or Wiles papers.