Strong lower bounds of the form $2^{(1-\epsilon)n}$, where $n$ is the number of variables and $\epsilon>0$ is arbitrarily small (i.e., bounds consistent with the Strong ETH), are exceptionally rare in proof complexity. The seminal work of Beck and Impagliazzo (STOC 2013) achieved such a bound for regular resolution, and the ... more >>>

Quantifying and understanding the complexity of mathematical proofs is a fundamental question in proof complexity. At the qualitative level, bounded arithmetic formalizes the notion of feasible proofs, where all functions implicit in proofs are from certain complexity classes. For instance, Cook's theory PV (STOC'75) captures proofs using only polynomial-time computable ... more >>>

We formalize AI alignment as a multi-objective optimization problem called $\langle M,N,\varepsilon,\delta\rangle$-agreement, in which a set of $N$ agents (including humans) must reach approximate ($\varepsilon$) agreement across $M$ candidate objectives, with probability at least $1-\delta$.
Analyzing communication complexity, we prove an information-theoretic lower bound showing that once either $M$ or ... more >>>