Articles on Hale's Kepler Conjecture proof

[Norman Megill]

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

[Ken Kubota]

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

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,

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

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

– Adams, Mark (2016): “HOL Zero’s Solutions for Pollack-Inconsistency”

http://www.proof-technologies.com/papers/hzsyntax_itp2016.pdf

Kind regards,

Ken Kubota

____________________________________________________

Ken Kubota

http://doi.org/10.4444/100

--
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+u...@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

[Mario Carneiro]

Certainly Metamath is Pollack consistent by this definition, since Norm has always been against hidden information in terms, and all major verifiers and IDEs for Metamath print formulas in the same format as the internal representation, which is as a whitespace-separated string of tokens. This is a controversial decision for other reasons ("What do you mean the formulas aren't trees?"), but Pollack consistency is one major benefit of this approach.

Mario

To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscribe@googlegroups.com.

To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

--
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+unsubscribe@googlegroups.com.

[Raph Levien]

To me the most interesting question posed by flyspeck is: what would it take to get this proof into Metamath? Conceptually, there shouldn't be much problem, you could take an OpenTheory trace of the HOL proof, and run that through one of the various efforts to interpret HOL in set theory. However, in practice this would be completely intractable. Given the reported scale of the verification in HOL, such a trace would likely be terabytes or perhaps even petabytes, and that's before conversion to Metamath.

I think it's possible to close that gap, and that it's an interesting problem to solve.

Raph

[fl]

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

When I read that I just wonder how long mathematics will remain a human activity? 

Transhumanism is the next step I suppose.

-- 

FL

[fl]

 

http://www.proof-technologies.com/papers/qed_paper.html

I really like the parts about the caveats related to the different checkers. They are rarely put forward obviously.

But here the author is honest.

Otherwise, I feel this very proof is numerically demanding. And that's the reason why HOL light was chosen.

It's sure not all the checkers could support that need.

-- 

FL

[Ken Kubota]

Hi Mark,

Thanks for your clarification in response to my email available online at
https://groups.google.com/d/msg/metamath/EOw1J-TG26k/dp9bB977AgAJ

Preventing removal or redefinition of existing definitions in R0
is an effective way of providing the property of faithfulness
[Adams, 2016, p. 21], as I believe.

From a logical point of view, the logical kernel should be as small as possible.
For this reason, in R0 definitions are, unlike in HOL and its variants,
only implemented in the printer and parser, but are _not_ part (an extension) of the logic,
as indicated in the email to John:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-October/msg00087.html
For comparison, the definitional principles in HOL require an additional rule
introducing an axiom (!) for each single definition,
see subsection 2.5.1 (Extension by constant definition) at
http://freefr.dl.sourceforge.net/project/hol/hol/kananaskis-11/kananaskis-11-logic.pdf

If you think that the property of faithfulness does not hold for R0, as claimed at
https://sourceforge.net/p/hol/mailman/message/35665823/
it would be helpful if you could provide a small counterexample.


Given the correctness of Mario's statement on Metamath at
https://groups.google.com/d/msg/metamath/EOw1J-TG26k/e6JLlvL9AgAJ
then currently HOL Zero, Metamath, and R0 are Pollack-consistent.

In R0, this concept (Pollack-consistency) is extended to whole proofs,
and also the property of faithfulness is provided.
Concerning this question, I haven't studied HOL Zero and Metamath yet.

Best regards,

Ken

____________________________________________________

Ken Kubota
http://doi.org/10.4444/100

> Am 25.06.2017 um 11:17 schrieb Mark Adams <ma...@proof-technologies.com>:
>
> 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+u...@googlegroups.com.
>>> To post to this group, send email to meta...@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-...@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info