This paper is a theoretical contribution, not a practical one, similar to Solomonoff Induction. Solomonoff Induction's contribution is essentially "there exists a formal mathematical process that inductive reasoning on evidence corresponds to" which, among other things, pretty much solves epistemological puzzles like the https://en.wikipedia.org/wiki/Raven_paradox from philosophy.

Yeah, the actual performance of Solomonoff Induction is uncomputable, but to me the useful point is that "induction can be done mathematically", and then what we do heuristically in our brains can be thought of as a low-fidelity analog of that. If I'm understanding the page correctly, this is the same idea but for statements based on proofs and logical theorems. Which seems to expand the scope somewhat.

(I'm really excited about this, actually, just as a person who enjoys learning about this stuff from Wikipedia. I feel like I've vaguely thought about how Solomonoff induction would work on statements that are derived from each other (or when combined with type-checking, since type-checking is closely related to theorem-proving), but had no idea how to even ask a precise question much less make anything of it.)