Hi Ken,
On 20/06/2017 12:38, Ken Kubota wrote:
This 2017 article by Thomas Hales et al. at _Forum of Mathematics, Pi_
seems to be identical with the 2015 article at:
https://arxiv.org/pdf/1501.02155.pdf
Yes, as far as I am aware, if there are any differences they are tiny.
Arxiv is a preprint service.
What I find even more interesting, is Mark's notion of
_faithfulness_,
Unfortunately my definition of "faithfulness" is a bit vague. See
below.
developing further Freek Wiedijk's notion of
_Pollack-consistency_ ("being able to correctly parse formulas that
it printed itself", quoted on p. 8).
Strictly speaking from Freek's original paper, being able to correctly
parse back printed formulas (i.e. forall tm. parse (print tm) = tm), is
called having a "well-behaved" parser/printer. In his paper,
"Pollack-consistency" is about not being able to derive "false" from
assuming the equality of formulae that get printed the same. But when
discussed, these concepts usually all get bundled together and described
as "Pollack-consistency".
It seems as if Mark’s HOL Zero and my R0 are the only
implementations that have this property of Pollack-consistency.
It's good to see that these properties are being taken seriously.
In the case of R0, this even holds for full proofs, and the
property of faithfulness is also implemented:
"Generally, definitions once introduced cannot be removed or
redefined (implementing the notion of 'faithfulness' as defined by
Mark Adams..)"
The intention with my use of the term "faithfulness" was to capture what
I understand others in the theorem proving community mean by the term.
Freek's defintions are really basic properties of parsers/printers that
users might naturally expect to hold, e.g. that parsing printed output
always results in the original internal term. But if a printer printed
"false" as "true" and "true" as "false", and the parser correspondingly
parsed "true" as "false" and "false" as "true", then this would satisfy
Freek's "well-behaved" property. So we need "faithfulness" to cover
that sort of thing. Banning deletion or redefinition of theory isn't
what I meant.
Mark.
Am 19.06.2017 um 23:15 schrieb Norman Megill <n...@alum.mit.edu>:
Some of you may be interested in the following.
A writeup of Hale's computer proof ("Flyspeck project") of the
Kepler sphere-packing conjecture has just been published:
T. Hale et. al, A Formal Proof of the Kepler Conjecture
https://www.cambridge.org/core/journals/forum-of-mathematics-pi/article/formal-proof-of-the-kepler-conjecture/78FBD5E1A3D1BCCB8E0D5B0C463C9FBC
A blog entry on this:
http://blog.journals.cambridge.org/2017/06/12/proving-the-kepler-conjecture/
The following paper discusses auditing issues for several proof
languages in the context of the above proof:
M. Adams, Proof Auditing Formalised Mathematics
http://www.proof-technologies.com/papers/qed_paper.html
Norm
--
You received this message because you are subscribed to the Google
Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it,
send an email to metamath+unsubscr...@googlegroups.com.
To post to this group, send email to metam...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
