Formal Theorem Proving

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, called Flyspeck, gives a complete formal proof of the Kepler conjecture in sphere packings.


Sign up to receive By the Numb3rs, the Department of Mathematics e-newsletter.

View past issues

Contact Us

The Dietrich School of
Arts and Sciences
301 Thackeray Hall
Pittsburgh, PA 15260
Phone: 412-624-8375
Fax: 412-624-8397