[FOM] The QED Manifesto today

[Timothy Y. Chow]

catarina dutilh <cdutilhnovaes at yahoo.com> wrote:
> Here is a question within the context of the recent discussions on the 
> ?QED Manifesto?: are the tools used for the fomalization of mathematics? 
> mentioned so far (Mizar, Isabelle, Coq etc.) mainly intended to 
> formalize proofs of theorems that have already been proved, or are they 
> also used to prove *new* theorems, i.e. to ?discover? mathematical facts 
> thus far unknown?

If you read Gonthier's account of the Coq proof of the 4-color theorem, 
you will see that along the way, they were driven to come up with new 
proofs (of what you might call "lemmas").  Similar stories will be told by 
anyone who has formalized any major theorem.  The pre-existing human proof 
is not always easy to convert directly to machine-checkable form, and it 
is often better to rethink the argument than to struggle to shoehorn the 
existing proof directly into the machine.

In this sense the aforementioned proof assistants do lead to the discovery 
of new mathematical facts.  However, the mechanism I described is 
different from what I think you are looking for.  What I think you want 
are examples where the computer more-or-less finds new facts on its own 
(like EQP's solution of the Robbins problem), rather than prompting the 
human to think creatively in ways that the human would not otherwise have 
done.  Although these particular proof assistants do have that capability 
in principle, they are not designed for that purpose (unlike Otter, MACE, 
etc.), so I would be surprised if there were any striking examples of that 
kind yet.  But I don't actively work in that area so maybe someone can 
correct me.

Tim