I have posted elsewhere the following thought:
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)?
With the answer being:
https://math.stackexchange.com/questions/4141341/problem-of-finding-shortest-proof-how-complex-is-it" 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. PA and 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 φ which has no proof of length ≤F(length(φ)). (Basically, we're looking at the Busy Beaver function in disguise when we talk about bounding proof searches ahead of time.)
With the above in mind, let us assume that a brute force algorithm doesn't exist that can circumvent the Busy Beaver function. Therefore, because of this does this necessarily mean that the alphabetical complexity of algorithms themselves are also unascertainable given the above?
I think the issue here is a confusion re: partial vs. total computable functions. (Below I fix some "appropriate ambient axiom system," say $\mathsf{ZFC}$ - so e.g. "theorem" means "$\mathsf{ZFC}$-theorem" and so on.)
Something which is often insufficiently emphasized in my experience is the extent to which partial (= defined on some subset of $\mathbb{N}$), rather than total (= defined on all of $\mathbb{N}$), are the starting point in computability theory. We assign to each Turing machine $M$ the function $f_M$ whose domain $D_M$ is the set of inputs on which $M$ halts and, for $m$ in that domain, $f_M$ is the value $M$ outputs eventually on input $m$. The functions we get in this way are the partial computable functions. (Really it should be "computable partial function," but oh well.) They are generally partial functions rather than total since $M$ may not halt on all inputs (= $D_M$ may be a proper subset of $\mathbb{N}$ - it could even be empty!).
Now amongst the partial computable functions, some are total (= $D_M=\mathbb{N}$) and some are not. (Meanwhile something like the Busy Beaver function is an example of a function which is total but not computable.) Totality is obviously a very nice property, but it's also very restrictive:
In fact something even more extreme (although it's ultimately due to the same underlying phenomenon) can occur:
OK, now let's look at your question.
The "proof length function" you're interested in is an example of Fact 2. Specifically, via brute-force-search, the following is a partial computable function: $$p(\#\varphi)=\begin{cases} \mbox{The length of the shortest $\mathsf{ZFC}$-proof of $\varphi$} & \mbox{if $\mathsf{ZFC}\vdash\varphi$}\\ \uparrow & \mbox{ otherwise}\\ \end{cases}$$
(Here "$\uparrow$" denotes "is undefined" and $\#\varphi$ is the Godel number of $\varphi$.) Note that the domain of $p$ is the set of (Godel numbers of) $\mathsf{ZFC}$-theorems, which is not all of $\mathbb{N}$, so $p$ really is partial.
This is utterly unproblematic. Note, however, that $p$ is not always defined. This makes sense: if I try to brute-force-search for a proof of a non-theorem $\varphi$, I'll just spin my wheels forever and not get anywhere. Granted, for some specific non-theorems there may be an easy argument that they are not provable from $\mathsf{ZFC}$, but $(i)$ I can't expect that in general (this is a consequence of Godel's theorem) and $(ii)$ regardless of point $(i)$, such cleverness isn't something the brute-force-searching-function $p$ does.
So all that is pretty simple. When we try to relate $p$ to total computable functions, however, things get a bit weird. While computable, $p$ grows extremely fast: for every total computable function $t$ there is some $n$ such that $p(n)\downarrow>t(n)$. (Here "$\downarrow>$" means "is defined and greater than.") This may feel absurd at first, but in fact is a key point illustrating just how much more "free" partial computable functions are than total computable functions.
Let me sketch a proof of the claim in the previous paragraph. I'm going to avoid mentioning the Busy Beaver function since it's really only useful as an analogy, and it seems to have made things more confusing.
Suppose I had a total computable function $f$ such that whenever $\varphi$ is a $\mathsf{ZFC}$-theorem it has a proof of length $<f(\#\varphi)$. (This is just saying that $f$ dominates $p$.) I can use this to check whether a sentence $\psi$ is consistent with $\mathsf{ZFC}$ in the first place: simply check all $\mathsf{ZFC}$-proofs of length $<f(\#\psi)$. If we find one whose conclusion is $\psi$ we know $\psi$ is a $\mathsf{ZFC}$-theorem, and conversely if $\psi$ is a $\mathsf{ZFC}$-theorem then it has a proof of length $p(\#\psi)<f(\#\psi)$ which we will find.
But once we have an algorithm for determining whether a sentence is consistent with $\mathsf{ZFC}$, we can solve the halting problem! Specifically, the sentence "$n$ is not in the halting problem" is consistent with $\mathsf{ZFC}$ iff $n$ is, in fact, not in the halting problem. This is because $\mathsf{ZFC}$ can "verify computations:" if a Turing machine $M$ halts on input $n$, then $\mathsf{ZFC}$ proves "$M$ halts on input $n$." (The analogous implication for "doesn't halt" is false, however.)
Since the halting problem is not computable, we've hit a contradiction.
Now you further asked how complicated $p$ is. It's a bit hard to answer this without a better sense of what is meant by "complicated," but here are some comments:
$p$ itself is a computable function. However, since it is not dominated by any total computable function, it doesn't lie in any of the usual complexity classes $\mathsf{P,NP,EXP,...}$ in any sense.
While $p$ is computable, we can separately ask how hard it is to dominate $p$ with a total (necessarily not computable) function. There turns out to be a very simple answer to this: the Turing degrees of total functions dominating $p$ are exactly those which are at least as complicated as the halting problem.