# Is there a short proof of the decidability of Kepler's Conjecture?

I've believed that the answer is "yes" for years, as suggested in various sources with reference to Tóth's work. For example, the Wikipedia article for Kepler Conjecture says:

The next step toward a solution was taken by László Fejes Tóth. Fejes Tóth (1953) showed that the problem of determining the maximum density of all arrangements (regular and irregular) could be reduced to a finite (but very large) number of calculations. This meant that a proof by exhaustion was, in principle, possible. As Fejes Tóth realised, a fast enough computer could turn this theoretical result into a practical approach to the problem.

However, Hales seems to contradict that answer in A Proof of the Kepler Conjecture (DCG Version):

Strictly speaking, neither L. Fejes Tóth’s program nor my own program reduces the Kepler conjecture to a finite number of variables, because if it turned out that one of the optimization problems in finitely many variables had an unexpected global maximum, the program would fail, but the Kepler conjecture would remain intact. In fact, the failure of a program has no implications for the Kepler conjecture. The proof that the Kepler conjecture reduces to a finite number of variables comes only as corollary to the full proof of the Kepler conjecture.

Since Hales says "reduces the Kepler conjecture to a finite number of variables", not "proves the decidability of the Kepler conjecture", let me now clarify what I mean by that, by example: A journal-quality paper proof, of let's say 50 pages, showing that the Kepler conjecture is reducible to a (not explicitly given) trillion-variable sentence of the Theory of Real Closed Fields, would be a "short proof of the decidability of Kepler's Conjecture". By reducible I mean an iff relationship. Hales's quote suggests that he and Ferguson did not furnish such a proof.

The problem remains decidable for sphere packings consisting of any fixed number of translates of a lattice. If one could prove that the optimal packing density in $$n$$ dimensions could be achieved using $$f(n)$$ lattice translates, for some computable function $$f$$, then the whole problem would become decidable. However, it’s unclear whether that is even true: perhaps optimal packings in high dimensions are not periodic at all. Even if it is true, it is well beyond what anyone knows how to prove. (No proof is known even if one assumes there is a periodic optimal packing.)