# zbMATH — the first resource for mathematics

Mathematical method and proof. (English) Zbl 1116.03012
The author discusses some aspects which are relevant to distinguish different proofs of the same theorem. As case studies, in the first part different proofs of three “classical” examples are analyzed: 1) Fermat primes; 2) products of sums of squares; 3) representability of sums of squares. In a second part it is shown how a certain concept of method (tactics) can be implemented – or represented – in the syntax of the proof system Isabelle [T. Nipkow, L. C. Paulson and M. Wenzel, Isabelle/HOL. A proof assistant for higher-order logic. Lect. Notes Comput. Sci. 2283. Berlin: Springer (2002; Zbl 0994.68131)].

##### MSC:
 03B35 Mechanization of proofs and logical operations 00A30 Philosophy of mathematics 00A35 Methodology of mathematics 03F07 Structure of proofs
##### Keywords:
Proof; Method; Tactics
##### Software:
Isabelle/HOL; Isabelle/Isar; Isar
Full Text:
##### References:
 [8] Bundy, A.: 1988, ’The Use of Explicit Plans to Guide Inductive Proofs’, in E. Lusk and R. Overbeek (eds.), 9th International Conference on Automated Deduction, Vol. 310 of Lecture Notes in Computer Science. Berlin, pp. 111–120. · Zbl 0656.68106 [9] Buss, S. R. (ed.): 1998, The Handbook of Proof Theory. North-Holland, Amsterdam. · Zbl 0898.03001 [10] Cauchy, A.-L.: 1821, Cours d’analyse de l’École Royale Polytechnique. Première partie: Analyse algébrique. Paris:. Reprinted in Cauchy’s Ouvres completes, Gauthier-Villars, Paris, 1882–1919, deuxième série, vol. 3. [11] Colton, S., A. Bundy, and T. Walsh: 1999, ’Automatic Concept Formation in Pure Mathematics’, in T. L. Dean (ed.), Automatic Concept Formation in Pure Mathematics. Proceedings of the 16th International Joint Conference on Artificial Intelligence. San Francisco, pp. 786–793. [12] Conway, J. H.: 1997, The Sensual (Quadratic) Form, Vol. 26 of Carus Mathematical Monographs, Mathematical Association of America, Washington, DC. · Zbl 0885.11002 [14] Corry, L.: 1996, Modern Algebra and the Rise of Mathematical Structures, Vol. 17 of Science Networks. Historical Studies, Birkhäuser Verlag, Basel. · Zbl 0858.01022 [16] Dedekind, R.: 1877, Sur la théorie des nombres entiers algébrique. Paris: Gauthier-Villars. Also Bulletin des sciences mathématiques et astronomiques (1), 11 (1876) 278–288, (2), 1 (1877) 17–41, 69–92, 144–164, 207–248; parts also in Dedekind’s Werke, vol. 3, 263–296. Translated as Theory of Algebraic Integers with an editorial introduction by John Stillwell, Cambridge University Press, Cambridge, 1996. [17] Dickson, L. E.: 1966, History of the Theory of Numbers. Vol. 1: Divisibility and Primality. Vol. 2: Diophantine Analysis. Vol. 3: Quadratic and higher forms. Chelsea Publishing Co, New York. Originally published by the Carnegie Institute of Washington, Washington, D.C., 1919–1923. [18] Ebbinghaus, H.-D., H. Hermes, F. Hirzebruch, M. Koecher, K. Mainzer, J. Neukirch, A. Prestel, and R. Remmert: 1990, Numbers, Vol. 123 of Graduate Texts in Mathematics, Springer-Verlag, New York. With an introduction by K. Lamotke, Translated from the second German edition by H. L. S. Orde, Translation edited and with a preface by J. H. Ewing. · Zbl 0705.00001 [21] Edwards, H. M.: 1996, Fermat’s Last Theorem: A Genetic Introduction to Algebraic Number Theory, Vol. 50 of Graduate Texts in Mathematics. Springer-Verlag New York. Corrected reprint of the 1977 original. · Zbl 0904.11001 [22] Euler, L.: (1732/3) 1738, ’Observationes de theoremate quodam Fermatiano aliisque ad numeros primos spectantibus’. Comm. Ac. Petrop. 6, 103–107. Reprinted in Volume 2 of Euler (1911–1956), pp. 1–5. [23] Euler, L.: (1747/48) 1750, ’Theoremata circa divisores numerorum’. N. Comm. Ac. Petrop. 1, 20–48. Reprinted in Volume 2 of Euler (1911–1956), pp. 62–85. [24] Euler, L.: 1770, Vollständige Anleitung zur Algebra. St. Petersberg: Kays. Akademie der Wissenschaften. Reproduced in Volume 1 of Euler (1911–1956). [25] Euler, L.: 1911–1956, Opera Omnia. Series Prima: Opera Mathematica. Geneva: Societas Scientiarum Naturalium Helveticae. 29 volumes. [26] Ferreirós, J.: 1999, Labyrinth of Thought: A History of Set Theory and its Role in Modern Mathematics, Vol. 23 of Science Networks, Historical Studies, Birkhäuser Verlag, Basel. · Zbl 0934.03058 [27] Gauss, C. F.: 1801, Disquisitiones Arithmeticae, G. Fleischer, Leipzig. [29] Gray, J.: 1992, ’The Nineteenth-century Revolution in Mathematical Ontology’, in Revolutions in Mathematics, Oxford Univ. Press, Oxford Sci. Publ. New York. pp. 226–248. · Zbl 0967.00508 [30] Hafner, J. and P. Mancosu: 2005, ’The Varieties of Mathematical Explanation’. K. Jørgensen et al., (Eds.) Visualization, Explanation, and Reasoning Styles in Mathematics, Kluwer. · Zbl 1159.00308 [31] Hardy, G. H. and E. M. Wright: 1979, An Introduction to the Theory of Numbers, 5th edn., Oxford. · Zbl 0423.10001 [32] Hermite, C.: 1848, ’Théorème relatif aux nombres entiers’. Journal de Mathématique pures et appliquées 13, 15. Reprinted in Hermite’s Ouevres, Gauthier-Villars, Paris, 1905–1917, p. 264. [33] Knobloch, E.: 1994, ’From Gauss to Weierstrass: Determinant Theory and its Historical Evaluations’. in The Intersection of History and Mathematics, Vol. 15 of Sci. Networks Hist. Stud. Birkhäuser, Basel. pp. 51–66. · Zbl 0817.01008 [35] Laugwitz, D.: 1999, Bernhard Riemann 1826–1866: Turning Points in the Conception of Mathematics, Birkhäuser Boston Inc, Boston, MA. Translated from the 1996 German original by Abe Shenitzer with the editorial assistance of the author, Hardy Grant, and Sarah Shenitzer. · Zbl 0931.01027 [36] Lemmermeyer, F.: 2000, Reciprocity Laws: From Euler to Eisenstein, Springer Monographs in Mathematics. Springer-Verlag, Berlin. · Zbl 0949.11002 [37] Lenat, D. B.: 1976, ’AM : An Artificial Intelligence Approach to Discovery in Mathematics as Heuristic Search’. Ph.D. thesis, Stanford. [40] Nipkow, T.: 2003, ’Structured Proofs in Isar/HOL’, in H. Geuvers and F. Wiedijk (eds.), Types for Proofs and Programs (TYPES 2002), Vol. 2646 of Lecture Notes in Computer Science. Berlin, pp. 259–278. Available under ”documentation” at http://www.cl.cam.ac.uk/Research/HVG/Isabelle/index.html · Zbl 1023.68657 [41] Nipkow, T., L. C. Paulson, and M. Wenzel: 2002, Isabelle/HOL. A Proof Assistant for Higher-order Logic, Vol. 2283 of Lecture Notes in Computer Science. Springer-Verlag, Berlin. · Zbl 0994.68131 [44] Scharlau, W. and H. Opolka: 1985, From Fermat to Minkowski: Lectures on the Theory of Numbers and its Historical Development, Undergraduate Texts in Mathematics, Springer-Verlag, New York. Translated from the German by Walter K. Bühler and Gary Cornell. · Zbl 0551.10001 [46] Smith, H. J. S., ’Report on the Theory of Numbers’. Originally published as a report to the British Association in six parts between 1859 and 1865. Reprinted by Chelsea both as a separate volume and in Smith (1965). [47] Smith, H. J. S.: 1855, ’De compositione numerorum primorum formae 4$$\lambda$$ + 1 ex duobus quadratis’, Journal für die reine und angewandte Mathematik (Crelle’s Journal) L., 91–92. Reprinted in Smith (1965), pp. 33–34. · ERAM 050.1326cj [48] Smith, H. J. S.: 1965, Collected Mathematical Papers, Chelsea Publishing Company, Bronx. Edited by J.W.L. Glaisher. Originally published by Clarendon Press, Oxford, 1894. [49] Stein, H.: 1988, ’Logos, Logic, and Logistiké’, in W. Aspray and P. Kitcher (eds.), History and Philosophy of Modern Mathematics. University of Minnesota, pp. 238–259. · Zbl 1366.00045 [51] Tappenden, J.: 1995, ’Extending Knowledge and ’Fruitful Concepts’: Fregean Themes in the Philosophy of Mathematics’. Noûs. · Zbl 1366.00050 [52] Troelstra, A. S. and D. van Dalen: 1988, Constructivism in Mathematics: An Introduction, vols. 1 and 2 North-Holland, Amsterdam. · Zbl 0653.03040 [54] Wenzel, M.: 1999, ’Isar – A Generic Interpretative Approach to Readable Formal Proof Documents.’, in Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Thèry (eds.), Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs’99, Nice, France, September, 1999, Proceedings, Vol. 1690 of Lecture Notes in Computer Science. Berlin, pp. 167–184. [55] Wenzel, M.: 2002, ’Isabelle/Isar – A Versatile Environment for Human-Readable Formal Proof Documents’. Ph.D. thesis, Institut für Informatik, Technische Universität München. [56] Wussing, H.: 1984, The Genesis of the Abstract Group Concept: A Contribution to the History of the Origin of Abstract Group Theory, MIT Press, Cambridge, MA. Translated from the German by Abe Shenitzer and Hardy Grant. · Zbl 0547.01001 [57] Zagier, D.: 1990, ’A One-Sentence Proof that Every Prime p (mod 4) is a Sum of Two Squares’, American Mathematical Monthly 97(2), 144. · Zbl 0735.11014 [58] ’The Isabelle theorem proving environment’, Developed by Larry Paulson at Cambridge University and Tobias Nipkow at TU Munich. http://www.cl.cam.ac.uk/Research/HVG/Isabelle/index.html .
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.