Ok? Why is this significant?

I don't know, what if someone made an app or a website where you get a dollar for every bit until an odd prime hits. The theorem says how much to price each spin to guarantee a long-term profit for the house (somewhere between tree fiddy and half a quadrillion dollars).

Actually, nothing practical, just sharing my love of math and excitement about the new possibilities of formal verification being unlocked.