Loading...

Prof. Thomas Hales - Lessons learned from the Formal Proof of the Kepler Conjecture

5,267 views

Loading...

Loading...

Transcript

The interactive transcript could not be loaded.

Loading...

Loading...

Rating is available when the video has been rented.
This feature is not available right now. Please try again later.
Published on Mar 29, 2012

Professor Thomas Hales, Mellon Professor at the University of Pittsburgh, gives a lecture entitled "Lessons learned from the Formal Proof of the Kepler Conjecture".

The Kepler Conjecture asserts that no arrangement of congruent balls in Euclidean space can have density greater than the familiar pyramid arrangement that is used to stack cannonballs. Sam Ferguson and Thomas Hale gave a computer-assisted proof of this conjecture in 1998, but a large team of referees was unable to certify the correctness of the proof after years of effort. A group of researchers is now developing a formal proof of Kepler's assertion, by formally certifying every algorithm and every last logical inference. This project is approaching completion, and this talk will discuss some of the lessons learned and will describe recent work by Solovyev on formal proofs of nonlinear inequalities.

Thomas C. Hales is the Mellon Professor of Mathematics at the University of Pittsburgh. In 1998, Hales, with the help of his graduate student Samuel Ferguson, proved Kepler's 1611 conjecture (and part of Hilbert's 18th problem) on the most efficient way to stack oranges. Hales's current project, called Flyspeck, seeks to formalize the proof of the Kepler conjecture in the computer proof assistant "HOL Light."

Recorded on Wednesday 21 March 2012.

Loading...

When autoplay is enabled, a suggested video will automatically play next.

Up next


to add this to Watch Later

Add to

Loading playlists...