Yes, there exist (uniformly constructible) polynomial-size Boolean formulas for threshold functions (which is how your functions are called). Equivalently, there are polynomial-size formulas for summing $n$ binary numbers of length $m$. Also equivalently, the complexity class (uniform) $\mathrm{TC}^0$ is contained in (uniform) $\mathrm{NC}^1$.
The easy way to do it is to use the so-called carry-save addition. This is a recursive construction whose basic step is a reduction of the computation of a sum of $3$ numbers $a,b,c$ to a sum of $2$ numbers $d,e$ using a linear-size constant-depth fan-in $2$ circuit (or formula): $d$ consists of bitwise sums of the inputs modulo $2$ disregarding any carries (i.e., the $i$th bit $d_i$ is $a_i\oplus b_i\oplus c_i$, where $\oplus$ denotes the parity function), whereas $e$ is the carry vector ($e_{i+1}=1$ iff $a_i+b_i+c_i\ge2$). By taking $n/3$ of these basic blocks in parallel, we can reduce a sum of $n$ numbers to a sum of $2n/3$ numbers by a constant-depth circuit, and by repeating this step $\log_{3/2}n$ times, we can sum $n$ numbers by a circuit of depth $O(\log n)$. Since a circuit of depth $d$ and fan-in $2$ with $k$ output bits can be expanded to a formula of size $k2^d$, this gives formulas of size $n^{O(1)}$.
In fact, threshold functions are also computable by polynomial-size log-depth monotone formulas (i.e., using only $\land$ and $\lor$, but not $\neg$), but this is harder to prove. A simple but nonconstructive probabilistic proof of the existence of such formulas was given by Valiant (Short monotone formulae for the majority function, J. of Algorithms 5 (1983), #3, 363–366). A constructive but very complicated construction follows from the construction of log-depth sorting networks by Ajtai, Komlós and Szemerédi (An $O(n\log n)$ sorting network, Proc. 15th STOC, 1983, 1–9).
