[FOM] The QED Manifesto today
gbuday at gmail.com
Mon Jan 26 17:25:49 EST 2009
Catarina Dutilh asks:
> 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?
The paper by Perlis et al describes mathematics as having short
theorems. Should we accept this, we can conclude that the new theorems
proven with proof assistants are not theorems of mathematics, as they
are about large definitions, e.g. the type soundness of a programming
language. And, is a theorem about a security protocol a theorem of
mathematics? A theorem about a floating-point hardware device? I guess
Pure mathematical theorems proved by proof assistants, like the
four-colour theorem are usually about known conjectures. Others might
cite an example of a new theorem, which I do not know.
More information about the FOM