[FOM] The QED Manifesto today
Timothy Y. Chow
tchow at alum.mit.edu
Wed Jan 28 13:53:42 EST 2009
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
More information about the FOM
mailing list