(See the sibling comment with a "10." in it for context.) 3. Completion of the Flyspeck project. What's the densest way to pack a huge number of oranges into a

(See the sibling comment with a "10." in it for context.) 3. Completion of the Flyspeck project. What's the densest way to pack a huge number of oranges into a huge box? Every greengrocer "knows" the answer: hexagonal close packing. (Actually, if you have too many oranges they will get squashed. Better use cannonballs or something.) The first person known to have conjectured explicitly that this is best was Johannes Kepler (better known for his work in astronomy) back in 1611. In 1990, a guy called Hsiang claimed to have proved this. It was (and is) generally reckoned that his proof had holes in it. One of the leading critics of Hsiang's proof was Thomas Hales, who in 1998 announced his own proof. It was a very computational proof: Hales reduced the Kepler conjecture to a statement about the minimum value of a function of 150 variables (presumably describing how the spheres are arranged; I don't know how this works, but I remark that Gauss proved back in 1831 that the densest arrangement with the spheres on a regular lattice is the usual one, so there's probably something clever going on), and then proved that there are "only" 5000 or so genuinely distinct configurations, each of which gives rise to a linear programming problem (i.e., optimization of a linear function subject to linear constraints), and then solved them all with a computer. This is a bit like the famous Appel-Haken proof of the "four colour theorem", only much worse. The mathematical details were extremely intricate. A lot of very smart mathematicians looked at Hales's proof and reported that they were 99% sure it was right but couldn't be more confident than that. So Hales started a project "FLysPecK" (= FormaL Proof of Kepler) to verify all the details using automated proof-checking software. (So there's a tenuous connection here with the "univalent foundations" work, but I don't think there's any more to it than that both are related to automated proof-checking.) And, after more than a decade of grind, the Flyspeck team has declared success and (assuming they haven't messed up) Kepler's conjecture has definitely been proved. What next? Well, presumably by applying proof-checking software to a real serious mathematical problem the Flyspeck team has helped to improve it and make it more useful for other real serious mathematical problems.