An explicit construction of short monotone formulae for the monotone symmetric functions

We construct formulae that assume the value 1 when and only when at least k of their n variables assume the value 1, using only conjunction and disconjunction, and having (for any fixed k) only

$\text{O}\text{(n}\text{log}\text{n)}\text{k}\text{2}{}^{\mathrm{<mtext>log</mtext><mtext>1n</mtext>}}$

occurences of variables.