|Automated Reasoning in Pure Mathematics|
|Instructor：||Thomas Hales [University of Pittsburgh]|
|Place：||Conference Room 3, Floor 2, Jin Chun Yuan West Building (近春园西楼2层第三会议室)|
Computers are becoming increasingly adept at constructing proofs in pure mathematics. This course will cover some of the fundamental algorithms in mechanical reasoning, starting with propositional and first order logic, then continuing with topics such as quantifier elimination procedures and Groebner bases. Lectures will cover the design of interactive proof assistants, which have been used to construct computer-checked proofs of theorems such as the Four Color Theorem, the Prime Number theorem, the Jordan curve theorem, and the Riemann mapping theorem.
Lectures will assume some degree of familiarity with the programming and operation of computers
Reference for the course:
J. Harrison, Handbook of Practical Logic and Automated Reasoning, Cambridge, 2009