Link should read --- https://www.cambridge.org/core/journals/forum-of-mathematics-pi/article/form...
From sect. 10 para -1 ---
(It seems to us that our single greatest vulnerability to error lies in the hand translation of this one statement from Isabelle to HOL Light, but even here there is no mathematical reasoning involved beyond a rote translation.) This bothered me as well. I'm not convinced that this work is a particularly significant development in the history of the Kepler conjecture; rather IMHO that projects of this nature represent the first reasonably promising steps in teaching research-level maths to a computer system. Incidentally, I haven't heard a great deal about Voevodsky and "Univalent Foundations" since they wangled their $7.5M from the DoD. Is anybody out there interested in that project? https://en.wikipedia.org/wiki/Homotopy_type_theory https://arxiv.org/pdf/1302.4731.pdf WFL On 6/18/17, rcs@xmission.com <rcs@xmission.com> wrote:
The Kepler Conjecture is that the usual sphere packing is optimal.
A report on the machine-verified proof of the Kepler Conjecture has been published. The proof is available, and can be checked with tolerable computing resources.
https://www.cambridge.org/core/journals/forum-of-mathematics-pi/article/ formal-proof-of-the-kepler-conjecture/78FBD5E1A3D1BCCB8E0D5B0C463C9FBC
The effort to make a formal machine-checkable proof turned into a major project. The author list for the report looks like it's for a big-science paper. The Kepler Conjecture is a very expensive theorem.
Rich
_______________________________________________ math-fun mailing list math-fun@mailman.xmission.com https://mailman.xmission.com/cgi-bin/mailman/listinfo/math-fun