[FOM] The QED Manifesto today

[Gergely Buday]

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
no.

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.

- Gergely