A de Morgan formula over Boolean variables $x_1, \ldots, x_n$ is a binary tree whose internal nodes are marked with AND or OR gates and whose leaves are marked with variables or their negation. We define the size of the formula as the number of leaves in it. Proving that some explicit function (in P or NP) requires large formula is a central open question in computational complexity. While we believe that some explicit functions require exponential formula size, currently the best lower bound for an explicit function is the $\tilde\Omega(n^3)$ lower bound for Andreev's function.

In this work, we show how to trade average-case hardness in exchange for size. More precisely, we show that if a function $f$ cannot be computed correctly on more than $\frac{1}{2} + 2^{-k}$ of the inputs by any formula of size at most $s$, then computing $f$ exactly requires formula size at least $\tilde\Omega(k) \cdot s$. The proof relies on a result from quantum query complexity by Reichardt [SODA, 2011]. Due to the work of Impagliazzo and Kabanets [CC, 2016], this tradeoff is essentially tight.

As an application, we improve the state of the art lower bounds for explicit functions by a factor of $\tilde\Omega(\log n)$.

Additionally, we present candidates for explicit simple functions that we believe have formula complexity $\tilde\Omega(n^4)$. In particular, one such function was studied in [Goldreich-Tal, CC, 2016] and is given by $F(x,y,z) = \sum_{i=1}^{n}\sum_{j=1}^{n}{x_i y_j z_{i+j}} mod 2$. Based on our main theorem, we give non-trivial super-quadratic lower bounds for these functions.