Are there any interesting mathematical problems that can be encoded with 5 states and 2 symbols, which now we can prove using BB(5)?
Actually, just as you can do bijective base-b [0], you can also do bijective Zeckendorf (using 1 and 2 with no two consecutive 1s). Although, as happens with bijective binary, bijective Zeckendorf is closely tied to ordinary Zeckendorf, so it doesn't offer much new. But bijective dual Zeckendorf doesn't work -- lots of numbers can't be represented!
One more fun fact about Zeckendorf and dual Zeckendorf: Write n>0 in Zeckendorf, and count how many zeroes it ends in. This will be even if the dual Zeckendorf representation of n ends in a 1, and odd if it ends in a 0. Similarly, if you write n in dual Zeckendorf and count how many 1s it ends in, this will be even if the (ordinary) Zeckendorf representation ends in a 0 and odd if it ends in a 1.
If you can encode a problem in n states, and you know BB(n), then, as you say, you could use that to solve the problem. Trouble is, how do you know BB(n)? In reality, the only way to determine BB(n) is to go and solve all such problems; there isn't any other easier method that you can apply that would then let you get answers for these problems as a consequence.
So, the value of BB(n) will always be a summation of "we did all the hard work of solving all the n-state problems", not something you do separately to get those answers out.