The Kepler conjecture asserts that the densest arrangement of congruent balls in Euclidean three-space is the face-centered cubic packing, which is the familiar pyramid arrangement used to stack oranges at the market. The problem was finally solved in 1998 by a long computer proof, The Flyspeck project seeks to give a full formal proof of the Kepler conjecture. This is an extended abstract for a talk in the formal proof session of ICMS-2010, which will describe the linear programming aspects of the Flyspeck project.
展开▼
