FOM: Relations between computer science and computer practice (as a whole) and mathematics

[Patrick Peccatte]

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