These lectures will be centered around a set of questions that can be loosely described as follows:
Are major open problems in Complexity Theory like $NP\stackrel ?\subseteq P/poly$ or $P\stackrel ?\subseteq NC1/poly$ independent from systems of Bounded Arithmetic? Do they possess efficient propositional proofs?
For obvious reasons (and it should be noted that we are deliberately working with the systems that, to the best of our knowledge, do prove all known results in Circuit Complexity) these independence questions are of utmost importance for both areas, Computational Complexity and Proof Complexity. Nonetheless, despite numerous efforts, they are still widely open. We will try to put these questions in the historical context and survey ideas (sometimes even with complete proofs) that have so far lead to at least non-negligible progress toward their solution. Although we will try to make the lectures as self-contained as possible, some familiarity with Circuit Complexity and Propositional Logic might be helpful. Also, the Introduction to http://www.mi.ras.ru/~razborov/res_k.ps can give a rather good impression of the set of topics we will be discussing.
Professor Alexander A. Razborov graduated from the Moscow State University (department for mathematics and mechanics) in 1985 and in the same year entered the graduate school of the Steklov Mathematical Institute of the Russian Academy of Sciences. He defended his PhD thesis (``On systems of equations in free groups'') in 1987, and his doctoral thesis (``Lower Bounds in the Boolean Complexity'') in 1991. Professor Razborov joined faculty of the Steklov Mathematical Institute in 1989 and have been working there since that. In 1999-2000 he was a Visiting Researcher at the Department of Computer Science of Princeton University, and in 2000-2008 he was holding a visiting position at the Institute for Advanced Study, Princeton. During his career, Professor Razborov worked in various areas including mathematical logic, computational complexity, proof complexity and combinatorics.