For first order theories, is it correct that there is a brute force algorithm that tells us the shortest proof length for any given theorem ('length' means the sum of the lengths of the formulas that appear as lines in the proof)?
Are there algorithms better than brute force? What is the complexity class for the problem?
There are two reasonable ways to measure the length of a proof: by steps or by symbols. For step-length, we can brute-force-search for proofs and be certain we've found the shortest one as long as our axiom system is finite - for symbol-length, we only need that the language is finite and our axiom system is computably axiomatized (e.g. $\mathsf{PA}$ and $\mathsf{ZFC}$).
That said, in either case we have a serious issue as far as complexity is concerned: as long as our axiom system is "sufficiently rich," for every computable function $F$ there is some theorem $\varphi$ which has no proof of length $\le F(length(\varphi))$. (Basically, we're looking at the Busy Beaver function in disguise when we talk about bounding proof searches ahead of time.)
That said, this doesn't rule out $(i)$ efficient proof search in simpler theories or $(ii)$ efficient proof search for particularly simple results. There's a rich literature on this topic, beginning with the already-interesting case of propositional proof search - "automated theorem proving" is a good keyword for this.