  Satisfiability solving has been used to tackle a range of long-standing open
math problems in recent years. We add another success by solving a geometry
problem that originated a century ago. In the 1930s, Esther Klein's exploration
of unavoidable shapes in planar point sets in general position showed that
every set of five points includes four points in convex position. For a long
time, it was open if an empty hexagon, i.e., six points in convex position
without a point inside, can be avoided. In 2006, Gerken and Nicol\'as
independently proved that the answer is no. We establish the exact bound: Every
30-point set in the plane in general position contains an empty hexagon. Our
key contributions include an effective, compact encoding and a search-space
partitioning strategy enabling linear-time speedups even when using thousands
of cores.
