But when cellphone adoption became widespread, it became necessary to figure out how to efficiently encode the signals of multiple cellular devices in the wireless spectrum in such a way that they do not interfere with each other. As it turns out, many of the mathematical techniques and insights generated by exploring these discrete and high-dimensional versions of the sphere packing problem have been of immense value for this problem - not just in the "positive" sense of designing efficient signal encoding methods, but also in the "negative" sense of also giving theoretical upper bounds on such efficiency, thus setting the right benchmarks to evaluate progress, and to avoid wasting resources on attempting encodings that are mathematically impossible.

(As a side note, the successful formalization of the proof of the Kepler conjecture has also inspired and informed many further collaborative formal projects, including my own experiments in this area, even if those projects do not directly involve sphere packing.)

Such contributions to tangible technological advances are subtle and indirect; but without such basic research, many such advances would have taken far longer to be developed, and some may not have been pursued at all. The cuts to funding for such reseearch - which will particularly impact the next generation of researchers - may save a few cents a year in the short term, but greatly reduce the capacity to solve many challenging technological problems of significant real-world impact in the future. (3/3)