$n^{O(\log \log n)}$ size monotone proofs of the weak pigeonhole principle

ABSTRACT. We present n^O(log log n) -size proofs in the (tree-like) monotone sequent calculus of the pigeonhole principle with (1 + ε)n pigeons and n holes, for ε = 1/polylog n. This improves on the bound of n^O(log n) inherited from proofs of the usual pigeonhole principle, with n + 1 pigeons and n holes, by Atserias et al., and supports the more general conjecture that the monotone sequent calculus polynomially simulates Hilbert-Frege systems.