There are no Platonic proofs - just correct or incorrect proofs.
> 4. In summary, Platonism is desirable in every way.
Modifying a remark by Bertolt Brecht:
Ask yourself: Does Platonism change the way you prove theorems?
If not - the problem is irrelevant,
If yes - you need Platonism.
> 3. Robots (verification systems) should be Platonists --- their statements
> should be about "sets" and "functions" and they should never
> talk about syntactic rules of inference when discussing "ordinary"
> mathematics.
This is important! Verification systems can (in general) only talk about rules of inference - but they should hide this carefully from the normal QED user. The same way your mailtool makes you think you read a letter when you are actually looking at a bitstream.
Ingo Dahn