|
Abstract |
In 1611, Kepler asserted that no packing of congruent balls in space can have density greater than the familiar cannonball arrangement. This statement, known as the Kepler conjecture, is now a theorem that has been formally verified. A theorem is formally verified if every step of the proof has been checked at the level of the primitive inference rules of logic and the foundational axioms of mathematics. This talk will present the Kepler conjecture, its proof, and background about the formal verification of theorems. |
