Worked solution: Flyspeck: a formal proof of the Kepler conjecture in HOL Light and Isabelle (2015)
The last move is bookkeeping: the traditional mathematical argument is formalised as one theorem that says 'if the tame-graph list is complete and these inequalities all hold, then the Kepler conjecture follows,' so plugging in the three separately verified computer results — like slotting the last three pieces into a machine whose blueprint has already been checked — finishes the proof.
The text part of the proof — the Marchal cell decomposition, the Cell Cluster Inequality, and the reduction to tame plane graphs — is formalised in HOL Light as a single theorem that only needs the nonlinear inequalities and the tame classification as black-box facts, exactly as displayed above. Combining that text theorem with the verified nonlinear inequalities (Step 6), the verified linear programs (Step 5), and the tame classification imported from Isabelle (Step 3) yields a complete formal proof that no packing of unit balls in can exceed the density of the face-centred cubic packing — the Kepler conjecture. The main statement can be replayed from a saved proof term in about forty minutes on an ordinary 2 GHz machine, an independent check any reader can run.