In a formal proof, all of the intermediate logical steps of a proof are supplied. No appeal is made to intuition, even if the translation from intuition to logic is routine. Thus, a formal proof is less intuitive and yet less susceptible to logical errors than a traditional proof.
In collaboration with a large international research group, Hales has completed one of the largest formal proof projects ever attempted. The project gives a complete formal proof of the Kepler conjecture in sphere packings.