Introduction to Formal Proof


Thomas Hales

University of Pittsburgh

Northeastern University

Thursday, February 12, 2009


Talk at 4:30 p.m. in 509 Lake Hall

Tea at 4:00 p.m. in 544 Nightingale Hall


Abstract:   A formal proof is a proof in which every logical inference has been checked all the way back to the fundamental axioms of mathematics. The number of primitive inferences can run into the millions, even for a traditional proof of modest size. A number of noteworthy theorems have now been checked formally, including the four-color theorem, the Jordan curve theorem, and the prime number theorem (both the elementary and analytic proofs). This talk will describe the current stage of development of formal theorem proving technology. It will describe some research projects aimed at bring formal theorem proving to every mathematician's desktop.

Here are some directions to Northeastern University. Lake Hall and Nightingale Hall can be best accessed from the entrance on the corner of Greenleaf Street and Leon Street. The two halls are connected, with no well-defined boundary in between. In particular, 509 Lake Hall is on the same corridor as 544 Nightingale Hall.

There is free parking available for people coming to the Colloquium at Northeastern's visitor parking (Rennaisance Garage). The entrance is from Columbus Avenue. If coming by car, you should park there and take the parking talon. After the lecture, you may pick up the payment coupon from Andrei Zelevinsky.

Home Web page:  Alexandru I. Suciu  Comments to:  
Posted:: January 27, 2009    URL: