*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Verify the legitimacy of a proof?*From*: Peter Lammich <lammich at in.tum.de>*Date*: Mon, 10 Jul 2017 11:10:54 +0200*In-reply-to*: <BD9ECBCD-B093-4F5F-91E1-8BF6714337B3@cam.ac.uk>*References*: <CADYF24fBE5-wFje-T9-z2c9Um4ZGf1y+ukaSiDi3EPa9uRBEaw@mail.gmail.com> <5b1c5907-c172-0e3d-6163-c70e0bc884c7@sketis.net> <CADYF24c9L7mdmpNspoSEinHGU-V-_w1axhYvsHqO4_cMnRhxnw@mail.gmail.com> <BD9ECBCD-B093-4F5F-91E1-8BF6714337B3@cam.ac.uk>

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. -- Â Peter

**Follow-Ups**:**Re: [isabelle] Verify the legitimacy of a proof?***From:*Lawrence Paulson

**References**:**[isabelle] Verify the legitimacy of a proof?***From:*scott constable

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

**Re: [isabelle] Verify the legitimacy of a proof?***From:*scott constable

**Re: [isabelle] Verify the legitimacy of a proof?***From:*Lawrence Paulson

- Previous by Date: [isabelle] Code equations get eta-contracted
- Next by Date: Re: [isabelle] State of the State Monad
- Previous by Thread: [isabelle] Concept of a small logical kernel, preserving logical dependencies, axiomatic type classes vs. type abstraction, Isabelle documentation â Re: Verify the legitimacy of a proof?
- Next by Thread: Re: [isabelle] Verify the legitimacy of a proof?
- Cl-isabelle-users July 2017 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list