The first talk, on Friday Dec 1, 11:45am, Princeton Theory Lunch Seminar Computer Science Building Rm 402.
In this talk I'll describe Haken's recent proof that Clique requires exponential size monotone circuits. I will explain the similarities and disticntions from Razborov's approximation method, using which such bounds were proved 10 years ago. A nice feature of Haken's proof is that it uses no nontrivial combinatorics.
The second talk, on Monday Dec 4, 1:45 pm, Institute for Advanced Study, Math building seminar room.
In that talk I'll describe Haken's breakthrough from 1985, proving that certain propositional tautologies, like the pigeonhole principle, require exponentially long resolution proofs. Resolution is a simple complete propositional proof system, often used in automated theorem proving.