Re: [isabelle] Verify the legitimacy of a proof?

On Sa, 2017-07-08 at 19:59 +0100, Lawrence Paulson wrote:
> "We have been given a proof of X; Is it credible?"

At this point, I second Ken. Although having human-readable machine
checked proofs is certainly a nice feature to get an idea of how a
proof works, the main points to check should be the statement of the
theorem, including the definitions (syntax tweaks, etc) it uses, as
well as the axioms its proof uses. Then, one relies on the logical
inference kernel that the proof is actually correct.
In particular, auxiliary lemmas and definitions only used for the
proof, but not in the main statement of the theorem, should be
irrelevant for trusting the theorem.

This principle should, in first place, be independent of whether the
user is malicious or not. However, in Isabelle, the malicious user has
a lot of possibilities to hide tweaks from a reviewer, while, in
HOLZero, these possibilities are very limited (if existent at all).

Actually, Isabelle contains many tools in this spirit, for example,
even the simplifier or classical reasoner apply some transformations on
the theorems provided to them. More high-level tools like function
package or datatype package even do really complex proofs, completely
hidden from the user.


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