Mathematical method and proof
type: Item
instance of: scholarly article
title: Mathematical method and proof
zbMATH Open document ID: 1116.03012
author: Jeremy Avigad
published in: Synthese
publication date: 2006-12-20T00:00:00Z
full work available at URL: https://figshare.com/articles/journal_contribution/Mathematical_Method_and_Proof/6492206
review text: 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)].
reviewed by: Reinhard Kahle
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 00A30
Mathematics Subject Classification ID: 00A35
Mathematics Subject Classification ID: 03F07
zbMATH DE Number: 5080794
zbMATH Keywords: Proof
zbMATH Keywords: Method
zbMATH Keywords: Tactics
describes a project that uses: Isabelle/HOL
describes a project that uses: Isabelle/Isar
describes a project that uses: Isar
MaRDI profile type: Publication
OpenAlex ID: W2044402378
cites work: Interpreting classical theories in constructive ones
cites work: Note on the generalization of calculations
cites work: The Warshall algorithm and Dickson's lemma: Two examples of realistic program extraction
cites work: Q3804239
cites work: Handbook of proof theory
cites work: Q4367590
cites work: Modern algebra and the rise of mathematical structures
cites work: Q3998810
cites work: The genesis of ideal theory
cites work: Mathematical ideas, ideals, and ideology
cites work: Q4207996
cites work: Labyrinth of thought. A history of set theory and its role in modern mathematics
cites work: The nineteenth-century revolution in mathematical ontology
cites work: The Varieties of Mathematical Explanation
cites work: Q3856819
cites work: Q4763296
cites work: Some logical metatheorems with applications in functional analysis
cites work: Q4253608
cites work: Q4956108
cites work: Mathematical explanation: problems and prospects.
cites work: Q4435474
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: On equivalents of well-foundedness. An experiment in MIZAR
cites work: Q3344253
cites work: Q5275453
cites work: Extending Knowledge and `Fruitful Concepts': Fregean Themes in the Foundations of Mathematics
cites work: Constructivism in mathematics. An introduction. Volume I
cites work: Q3338169
cites work: A One-Sentence Proof That Every Prime p≡1(\mod 4) Is a Sum of Two Squares
DOI: 10.1007/S11229-005-4064-5
Recommended article: Mathematical proof
Recommended article: Mathematical proofs
Recommended article: Q3070952
Recommended article: Q3633204
Recommended article: Q4371509
description: scientific article; zbMATH DE number 5080794