Mathematical method and proof (Q857692)

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 [\textit{T. Nipkow, L. C. Paulson} and \textit{M. Wenzel}, Isabelle/HOL. A proof assistant for higher-order logic. Lect. Notes Comput. Sci. 2283. Berlin: Springer (2002; Zbl 0994.68131)].