http://en.wikipedia....ki/Thomas_Hales
http://en.wikipedia....pler_conjecture
http://www.math.ac.v...07.htm#lecture7
September 14, 2007:
Speaker: Prof. Thomas Hales, University of Pittsburgh
Title: From Formal Proof to Geometry
Place: Auditorium Room 301, Building A5
Time: 9:00
Abstract: In a formal proof, every step of a proof is checked, all the way back to the fundamental axioms and rules of inference of mathematics. A formal proof is often less intuitive than an ordinary proof, but it is also less prone to errors. In recent years, a number of nontrivial theorems have been checked formally, including the proof of the four-color theorem, the prime number theorem, and the Jordan curve theorem. This talk will describe some of these formal proofs. Another project, called the "FLYSPECK" project aims to formalize significant parts of discrete geometry, including the proof of the Kepler conjecture on sphere packings.
