Forty-five points that cannot be covered by disjoint unit disks: a computer-assisted proof

Imagine a finite set of points on a table and a supply of identical round coins. The pointsare coverable if the coins can be laid down, without overlapping (touching is allowed), sothat every point lies under some coin. Let σ be the largest number such that every set ofσ points is coverable. It is known that 12 ≤ σ ≤ 49: Aloupis, Hearn, Iwasawa and Uehara(2012) showed that any 12 points can be covered and constructed, with a proof by hand, 50points that cannot. In the same paper they described a configuration of 45 points on threeconcentric circles, with 3, 21 and 21 points, and reported that a computer search had foundno covering; a proof was not given. Their description fixes the radii and the numbers ofpoints but not how the three circles are turned relative to each other. We take the versionin which the two large circles are aligned point by point and one inner point lies on the sameray as a point of each large circle, and we give a rigorous computer-assisted proof that thisset of 45 points cannot be covered. Consequently σ ≤ 44. The proof first uses elementarygeometry to reduce the problem to a finite search, and then carries out two searches bycomputer in which every step that rules something out is checked with interval arithmetic,so that rounding errors cannot produce a false conclusion. The whole computation takesabout 20 minutes on two processor cores. We also test the programs on configurations thatare known to be coverable, where they correctly fail to rule out the true coverings, and weshow with exact certificates that every 44-point subset of the configuration is coverable.