# Upper bound of Frege proofs length

I read no superpolynomial lower bound is known for the length (number of symbols) of zeroth order logic Frege proofs. My question is: what is the best upper bound known? I.e. given a tautology $$f$$ of length $$n$$, what length is sufficient to prove $$f$$?