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 >>>

We initiate a systematic study of the computational complexity of property testing, focusing on the relationship between query and time complexity. While traditional work in property testing has emphasized query complexity—often via information-theoretic techniques—relatively little is known about the computational hardness of property testers. Our goal is to chart the ... more >>>