Mathematics Colloquia and Seminars

Return to Colloquia & Seminar listing

Computer Verification and Math

Distinguished Lecture Series

Speaker: Thomas Hales, University of Pittsburgh
Related Webpage: http://www.math.ucdavis.edu/seminars/thurston/
Location: 1147 MSB
Start time: Thu, May 10 2018, 4:30PM

The use of large-scale computer calculations in the traditionally paper-and-pencil discipline of mathematics has prompted researchers to reevaluate the whole idea of what makes a proof.
A conjecture by Kepler in 1611 asserts that the densest arrangement of spheres is the familiar pyramid shape used to stack oranges at fruit stands.
In 1998, Samuel Ferguson and I announced a proof of the conjecture, consisting of nearly 300 pages – plus at least 40,000 lines of custom computer code. The journal Annals of Mathematics assigned a dozen referees to check that there was not a single error anywhere in this proof. But when the proof was finally published, the editor conceded that referees could not certify its correctness "because they have run out of energy to devote to the problem."
In response, I organized a project to have computers referee the correctness of computer calculations. Unlike humans, automated referees do not run out of energy.



Reception preceding the talk at 4pm.

This talk is intended for a general audience. Part of the Thurston Lecture Series.