Mathematical proofs can be classified using the computational complexity of concepts that are used in the proof. We are expecially interested in proofs of mathematical theorems that are important in computer science. These include first of all those theorems that state the correctness of algorithms, which in turns often require other, well established theorems from various areas of mathematics, such as linear algebra, discrete mathematics, number theory, etc. For example, the correctness of RSA encryption requires Fermat's Little Theorem. Studying the proof complexity of these theorems is the subject of a recently emerged research program called Bounded Reverse Mathematics.
This talk is an introduction to this research program.
Phuong Nguyen received his PhD from University of Toronto in 2008, under the supervision of Professor Stephen Cook. His research interests are in complexity theory and mathematical logic. He has received a number of competitive scholarships and fellowships, including the Australian Government's AusAID scholarship, the Eduard Cech Center for Algebra and Geometry postdoctoral fellowship, and the Natural Sciences and Engineering Research Council of Canada postdoctoral fellowship. He has co-authored with Professor Cook a book titled "Logical Foundations of Proof Complexity" which is published by the Cambridge University Press in 2010. Phuong Nguyen was awarded a Silver Medal in the International Mathematical Olympiad in 1995.