[FOM] The QED Manifesto today

[catarina dutilh]

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? In other words, are they also used as tools for discovery, or only as tools for verification? Can anyone mention a *surprising* result (in the sense of going against what was intuitively thought before the proof), attained exclusively by means of one of these tools?

As a general thing, I am very interested in surprising, counterintuitive results (in logic or mathematics) attained largely or exclusively by means of the ‘blind’ manipulation of formalisms, so I would be grateful if people could mention examples of such cases.

Thanks,

Catarina (ILLC -- University of Amsterdam)