A New Style of Mathematical Proof

  • William M. FarmerEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10931)


Mathematical proofs will play a crucial role in building a universal digital mathematics library (UDML). Traditional and formal style proofs do not adequately fulfill all the purposes that mathematical proofs have. We propose a new style of proof that fulfills seven purposes of mathematical proofs. We believe this style of proof is needed to build a highly interconnected UDML.


Mathematical proof Traditional proof style Formal proof style Universal digital mathematics library Little theories method Theory graphs Flexiformalization Cross checks 



The author would like to thank the referees for their comments. This research was supported by NSERC.


  1. 1.
    Barwise, J., Seligman, J.: Information Flow: The Logic of Distributed Systems. Tracts in Computer Science, vol. 44. Cambridge University Press, Cambridge (1997)CrossRefGoogle Scholar
  2. 2.
    Farmer, W.M., Guttman, J.D., Javier Thayer, F.: Little theories. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 567–581. Springer, Heidelberg (1992). Scholar
  3. 3.
    Kohlhase, M.: The flexiformalist manifesto. In: Voronkov, A., Negru, V., Ida, T., Jebelean, T., Petcu, D., Watt, S.M., Zaharie, D. (eds.) 14th International Workshop on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2012), pp. 30–36. IEEE Press (2013)Google Scholar
  4. 4.
    Kohlhase, M.: Mathematical knowledge management: transcending the one-brain-barrier with theory graphs. Eur. Math. Soc. (EMS) Newsl. 92, 22–27 (2014)MathSciNetzbMATHGoogle Scholar
  5. 5.
    Kreisel, G.: Some uses of proof theory for finding computer programs. In: Colloque international de logique: Clermont-Ferrand 18–25 juillet 1975, Colloques internationaux du Centre national de la recherche scientifique, vol. 249, pp. 123–133. Centre national de la recherche scientifique (1977)Google Scholar
  6. 6.
    Kreisel, G.: Mathematical logic: tool and object lesson for science. Synthese 62, 139–151 (1985)MathSciNetCrossRefGoogle Scholar
  7. 7.
    Lakatos, I.: Proofs and Refutations. Cambridge University Press, Cambridge (1976)CrossRefGoogle Scholar
  8. 8.
    Rav, Y.: Why do we prove theorems. Philosophia Mathematica 7, 5–41 (1999)MathSciNetCrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.McMaster UniversityHamiltonCanada

Personalised recommendations