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. 
 A: I don’t believe any short proof is known for the decidability of the Kepler conjecture, or indeed any proof other than Hales’s proof and its descendants. The issue is exactly what Hales explains in the quotation: the strategy is to reduce the problem to an inequality involving only finitely many variables, but this inequality is considerably stronger than the original conjecture. If it were to fail, that would not imply that Kepler’s conjecture is false.
Similarly, decidability is not known for the conjectured optimum in four dimensions, or any other case in which the sphere packing problem has not been solved.
For comparison, the lattice packing problem (where the spheres must be centered at the points of a lattice) is decidable. However, good packings are not necessarily lattices, so this does not imply that the full sphere packing problem must be decidable
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.)
The question of how much periodic structure we should expect in an optimal packing is really fundamental, as is decidability more generally, and any progress would be great. 
