[math-fun] report on proof of the Kepler Conjecture

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