Proof analysis is a new domain in which the methods of structural proof theory, developed mainly for systems of pure logic, are extended to cover mathematical theories. The idea is to present mathematical axioms as rules of proof, with the aim of obtaining a complete control over all the possible combinations of these rules. Typical consequences of such control contain positive solutions to word problems, old and new. The lectures begin with a brief presentation of systems of logical proof and of the central methods of the structural analysis of logical proofs. Next it is shown how such purely logical systems can be extended with rules that correspond to mathematical axioms. This is done so that parts of proofs with mathematical rules are completely separated from parts with the rules of logic. The latter can be set aside for good, after which we can study the combinatorial possibilities offered by a system of rules of a mathematical theory. We begin with the theories of equality and order. As an illustration of the method of proof analysis, we consider Szpilrajn's theorem by which a partial order can be extended into a linear one. Such extension theorems typically turn into what are called conservativity theorems in logic: In this case, it can be be defined very precisely what the linearity of order amounts to, with the result that in the absence of what it amounts to, the linearity postulate is not needed. The results is proved through a proof transformation that eliminates the applications of linearity in proofs. Work on proof analysis has led to two or three basic variants of the method. One very useful method emulates what is in logical systems called natural deduction. This method is applied to lattice theory: It is shown that the rules of lattice theory can be permuted to a certain standard order, with a very concise combinatorial solution of the uniform word problem as a principal result. A long-standing open problem, namely the uniform word problem for ortholattices, is solved by the same method. Other applications of the method of proof analysis cover such topics as plane projective and affine geometry. Finally, time permitting, the methods developed for mathematical theories are applied to systems of logic, such as modal and temporal logics.