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.