[FOM] SHIFTING PARADIGMS?

[Josef Urban]

On Jul 28, 2014 9:50 PM, "Timothy Y. Chow" <tchow at alum.mit.edu> wrote:
>
> 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?

I think there is still a lot of work to generate interesting conjectures
and to automatically find their proofs in fields that are (considered) much
less "computational" than for example number theory - say general topology,
measure theory, set theory, functional analysis, etc.

There is some seminal work on general conjecture making in number theory
(Lenat - AM) and perhaps graph theory (Fajtlowicz - Graffiti), but I don't
think we have shown how to do this for most of math. And even if the
conjecture-generating part was not so hard, we are nowhere near finding
proofs of new interesting conjectures in most of math automatically i is
important if you suddenly generate thousands of them) . We are happy that
we can now automatically discharge a decent part of small lemmas in
existingiii formal math libraries.

Josef

>
> Tim
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20140729/9889271e/attachment.html>