@tao@mathstodon.xyz This seems predicated on the notion that the Companies (who have little to no intrinsic interest in the mathematics itself) would continue to invest their resources in producing theorems. Do you see that continuing indefinitely? Maybe it's my own lack of imagination, but I'm struggling to envisage any long-run founts of theorems having no intrinsic mathematical motivation, which would necessitate such a regime. (I somehow prefer not to phrase this comment in terms of the analogy.)