From Kepler to Hales, and back to Hilbert (Q1946041)

Kepler's conjecture on tight packing from 1611, turned into a finite optimization problem by László Fejes Tóth in 1953, has been recently proved by \textit{Thomas C. Hales} (announced in 1998, published in [Ann. Math. (2) 162, No. 3, 1065--1185 (2005; Zbl 1096.52010)]). The paper presents the conjecture, its reduction to a nonlinear optimization problem over a compact set, and Hales's simplification of that reduction which ``resulted in a manageable computation, albeit an enormous one'' (reduction and simplification without details). The main part of the paper consists of comments on the expected impact of Hales's approach, which the author sees in moving from the classic paradigm of proving to a new one in the formalist spirit of Hilbert, ``most likely forever''. The prophecy sounds audacious, but there is some weight in it.