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
<https://arxiv.org/pdf/1501.02155.pdf>
Maybe co-author Mark Adams (who is on the HOL list) would like to comment on
this.
In my overview at http://doi.org/10.4444/100.111
<http://doi.org/10.4444/100.111>,
I tried to summarize the Flyspeck project at the end of section 1
(currently p. 4 and footnote 9), crediting Mark's HOL Zero appropriately,
and referring to the 2015 article.
What I find even more interesting, is Mark's notion of faithfulness, developing
further Freek Wiedijk's notion of Pollack-consistency
("being able to correctly parse formulas that it printed itself", quoted on p.
8).
It seems as if Mark’s HOL Zero and my R0 are the only implementations
that have this property of Pollack-consistency. 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 in [Adams,
2016, p. 21].)"
http://www.owlofminerva.net/files/README.txt
<http://www.owlofminerva.net/files/README.txt>
However, I haven't studied Metamath yet.
Both papers are available online:
– Wiedijk, Freek (2012): “Pollack-inconsistency”
http://www.sciencedirect.com/science/article/pii/S157106611200028X/pdf?md5=04ceb92a245b5bde8c4eca0610032293&pid=1-s2.0-S157106611200028X-main.pdf
<http://www.sciencedirect.com/science/article/pii/S157106611200028X/pdf?md5=04ceb92a245b5bde8c4eca0610032293&pid=1-s2.0-S157106611200028X-main.pdf>
– Adams, Mark (2016): “HOL Zero’s Solutions for Pollack-Inconsistency”
http://www.proof-technologies.com/papers/hzsyntax_itp2016.pdf
<http://www.proof-technologies.com/papers/hzsyntax_itp2016.pdf>
Kind regards,
Ken Kubota
____________________________________________________
Ken Kubota
http://doi.org/10.4444/100 <http://doi.org/10.4444/100>
> 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
> <mailto:metamath+unsubscr...@googlegroups.com>.
> To post to this group, send email to metam...@googlegroups.com
> <mailto:metam...@googlegroups.com>.
> Visit this group at https://groups.google.com/group/metamath
> <https://groups.google.com/group/metamath>.
> For more options, visit https://groups.google.com/d/optout
> <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
