[FOM] SHIFTING PARADIGMS?
Timothy Y. Chow
tchow at alum.mit.edu
Mon Jul 28 13:55:54 EDT 2014
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?
More information about the FOM