The formal proof of the Kepler conjecture

The Kepler conjecture asserts that no packing of congruent balls in space can have density greater than the familiar cannonball arrangement. If every
logical inference of proof has been checked all the way to the fundamental axioms of mathematics, then we say that the proof has been formally veried.
The Kepler conjecture has now been formally veried by computer, in a massive cloud computation. This talk will report on this and other massive
formal verication projects.