[FOM] SHIFTING PARADIGMS?

[Timothy Y. Chow]

Dana Scott wrote:

> But here is my prediction today: Big Proofs will soon show that 
> computers and logic have to be used TOGETHER to make progress in certain 
> areas of mathematics. That is, we need to show convincingly how
>
>  COMPUTER-ASSISTED PROOFS APPLY TO MATHEMATICS.
[...]
> What is needed -- in my personal view -- are mathematical DISCOVERIES 
> made while doing computer- aided proofs -- where the new facts ARE 
> surprising. The hard reality seems to be that the mathematics community 
> will not pay very much attention to new tools in logic unless they can 
> see them as essential for making new discoveries.

I would like to understand in what sense you think that this paradigm 
shift has *not yet* occurred.

Large computer computations are already used routinely to discover new 
mathematics.  This is the field of "experimental mathematics."  The 
computations are not just used to generate raw material for conjectures 
(although that is an important part of it); the computations are also used 
in the proofs.  It is routine to trust that a computer algebra package has 
correctly performed some calculation that is an essential part of a proof.

What else do you think is still missing?

Tim