Prolegomena to any theory of proof simplicity

Research output: Contribution to journalArticlepeer-review

5 Scopus citations


By looking at concrete examples from elementary geometry, we analyse the manner in which the simplicity of proofs could be defined. We first find that, when presented with two proofs coming from mutually incompatible sets of assumptions, the decision regarding which one is simplest can be made, if at all, only on the basis of reasoning outside of the formal aspects of the axiom systems involved. We then show that, if the axiom system is fixed, a measure of proof simplicity can be defined based on the number of uses of axioms deemed to be deep or valuable, and prove a number of new results regarding the need to use at least three times some axioms in the proof of others. One such major example is Pappus implies Desargues, which is shown to require three uses of Pappus. A similar situation is encountered with Veblen’s proof that the outer form of the Pasch axiom implies the inner form thereof. The outer form needs to be used at least three times in any such proof. We also mention the likely conflicting requirements of directness of a proof and the length of a proof.

Original languageEnglish (US)
Article numberY
JournalPhilosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences
Issue number2140
StatePublished - Mar 11 2019


  • Direct proof
  • Elementary geometry
  • Hilbert’s 24th problem
  • Multiple uses of axioms
  • Ordered geometry
  • Simple proofs

ASJC Scopus subject areas

  • General Mathematics
  • General Engineering
  • General Physics and Astronomy


Dive into the research topics of 'Prolegomena to any theory of proof simplicity'. Together they form a unique fingerprint.

Cite this