The original slides ↓:
The slides together with my notes during the talk on June 9th:
Corrections and remarks:
On page 6 of the slides, I should have referred the following papers:
Krajíček, J., Pudlák, P., & Woods, A. (1995). An exponential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle, Random Structures and Algorithms, 7(1), 15-39.
Pitassi, T., Beame, P., & Impagliazzo, R. (1993). Exponential lower bounds for the pigeonhole principle, Computational Complexity, 3(2), 97-140.
The original work of Ajtai gave a superpolynomial lower bound for the pigeonhole principle over constant-depth Frege system, and the papers above improved the lower bound to exponential order.
For more information, see section 15.7 of:
Krajíček, J. (2019). Proof complexity. Cambridge, UK: Cambridge University Press, Encyclopedia of Mathematics and Its Applications 170.