I am interested about the minimal size (number of gates) of a family of circuits (with negation) over a complete Boolean basis (with fanin 2) that computes some explicit Boolean function. (In other words, I want results that apply for a specific function, not diagonalization, counting, or non-constructive arguments). I call $n$ the number of inputs.
Section 1.5.2 of Boolean Function Complexity by Stasys Jukna (2011) says that the best such lower bound currently known is in $5n - \text{o}(n)$, from Iwama and Morizumi in 2002. This is very surprising, because, as Shannon proved in 1949 by a counting argument, most Boolean functions require exponential-size circuits.
Is the $5n - \text{o}(n)$ result still the best known? Is there any reason why proving a super-linear lower bound on the circuit size of an explicit function seems out of reach? In particular, do we know that solving this would close long-standing open problems in complexity theory as well?
