Is Solomonoff induction a theorem for making optimal probability distributions or a definition of them? That is to say, has anyone proved that Solomonoff induction produces probability distributions that are "optimal," or was Solomonoff induction created to formalize what it means for a prediction to be optimal. In the former case, how could they define optimality?

(And another question: I posted this a couple days ago on the last open thread, but it was closed before I got a response. Is it okay to repost it?)