It's not. Godel is asking, what's the fastest program that can tell if a (first order predicate logic) formula is provable? Maybe you were confused by the 'max

It's not. Godel is asking, what's the fastest program that can tell if a (first order predicate logic) formula is provable? Maybe you were confused by the 'max', but what he's doing is defining the complexity of the prover by the hardest (max computational time) formula instance for each length n. You still try to handle that maximum difficulty case as efficiently as possible, it just happens to take the longest.