[Date Index] [Thread Index] [FOM Postings] [FOM Home]

*To*: fom <fom@math.psu.edu>*Subject*: FOM: Relations between computer science and computer practice (as a whole) and mathematics*From*: Patrick Peccatte <peccatte@club-internet.fr>*Date*: Thu, 10 Dec 1998 21:42:52 +0100*Reply-To*: peccatte@club-internet.fr*Sender*: owner-fom@math.psu.edu

The recent discussion on certainty comparing "purely human proofs" and "computer-assisted proofs" leads us to examine a broader corpus of the relations between mathematics and computers from a philosophical point of view. This include: 1. Computer device considered as an implementation of mathematical device. This is the first thesis of Anatoly Vorobey (20 nov 1998 06:07:38). It is well known that computer science is now a branch of mathematics by right. But the affirmation above must be compared to the situation in empirical sciences where nobody serious says that physics is a 'concrete crystallisation' of some chapter of mathematics. 2. The extension of the Quine-Putnam indispensability argument from empirical sciences to computer science. 3. The Curry-Howard correspondence. The 'formulae-as-types' and 'proofs-as-programs' is not a way of speaking. This is an isomorphism, a mathematical object which is of great importance for our comprehension of mathematics. I am astonished that this subject (to my knowledge) has not been discussed here. 4. Proof checkers. The distinction between this class and the following has been noted by Randy Pollack (02 dec 1998 18:42:56). 5. Computer assisted-proofs. I agree fully with Joe Shipman (07 dec 1998 13:34:42). The length of proof is certainly not the only criterion to compare human proofs and computer-assisted proofs. And despite the fact that there exist comparatively many less computer-assisted theorems than classical theorems, I should appreciate any comment on other proofs like Waring problems, searching Golomb rules, double-bubbles, the Lam theorem in projective geometry, etc. 6. Exhibition of big or complicated mathematical objects via computers like the Chaitin's equation. 7. Limitation theorems considered from the point of view of the information theory (i.e. the algorithmic information theory). This has been criticized by Don Fallis: The source of Chaitin's incorrectness, Philosophia mathematica (3) vol. 4 (1996), pp. 261-269. 8. The Wilf-Zeilberger algorithmic theory of proof as exposed for example in the book A=B (Petkovsek-Wilf-Zeeilberger, A.K. Peters, 1996). 9. Experimental mathematics (cf. CECM). 10. Analogies between mathematical practice and computer practice. These relations are more diversified and deeper than a too simple and widespread conception that 'computer-is-only-a-tool-for-mathematics-like-paper-and-pencil'. These relations seem at least as deep as the traditionally privileged relations between mathematics and physics. And I should try to think them as a whole (i.e. both computer science and computer practice relationships with mathematics) and not only with a focus on computer-assisted proofs vs purely human proofs. Comments are welcome to extend these topics and analyze their relevance for fom. -- Patrick Peccatte http://peccatte.rever.fr

[Date Prev] [Date Next] [Thread Prev] [Thread Next]

[Date Index] [Thread Index] [FOM Postings] [FOM Home]