Re: [isabelle] lexical matters



> 
> We should remember that at the moment it is very easy for someone to
> maliciously produce what appears to be a formal proof of some statement but
> is in fact something that takes advantage of the sorts of pretty printer
> problems I am talking about.  Now if theorem provers are ever going to make
> it big, we are then in the situation where commercial pressures, etc, are
> pushing people to claim they have proved something when they have in fact
> not.  One of the important roles of a theorem prover should be as a highly
> trustworthy tool to support a human proof auditor checking that some huge
> 10,000 line proof of a theorem does indeed establish the theorem.

I don't think this is a problem in practice. Theorem provers are already used in big certification projects. The evaluators in such projects usually know what they are doing, at least up to the level where they would easily be able to spot attempts to make syntactically misleading proof statements. It's easy enough to scan for ML blocks or similar in theory files, spot duplicate identifiers, etc, and demand good explanations for their presence (or just forbid them). And the threat of just using a proof checker is always there, so why try to cheat on syntax? 

I'm with Larry on this: the much bigger problem is to convince yourself that the model and final theorem are in any way useful or right. This is where cheating will happen much earlier. 

Cheers,
Gerwin




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.