I can see it happening if people start depending AI-generated proof libraries for the work they are interested in. Not because the libraries are proprietary, but because they are impenetrable. AI usage wouldn't result in this directly, but it could be a consequence of formal verification as a substitute for canonicalization in some cases.

(Disclaimer: I had quite a bit of formal training in mathematics at one point, but have worked in software for more than two decades now. I wasn't on the applied side, but I recall that MATLAB evoked similar concerns back in the day.)

I'm not a mathematician or any other kind of scientist. Just a toiler in the software mines, and an onlooker.

> It goes entirely against the culture of research mathematics to hoard secrets. If you've done something interesting, you want to share it, and it's in your best interest to share it.

You're describing an enviable human culture with a reward system suited to people. People publish papers etc. to enrich the human domain and to get recognition. AIs don't care about things - and neither, I'm asserting, will their owners. That culture will become a vestige.

Mathematics as the underpinning of science and technology that can be exploited for inter-state competition, including cryptography but not limited to that (image analysis, targeting algorithms, conflict modelling, whatever) won't see the light of day. The AIs that discover the mathematics will be paid for by the warfighting budgets of states, and by the corporations that feed on them.

There could be a difference between academic mathematical research and commercial mathematical research, just as in the difference between FOSS and commercial code. Perhaps the difference lie between pure math and applied math with applied math having more incentive for secrecy given that large swaths of computing is just applied math in fancy wrappers.

If you can derive some special formula that prints money from accurate prediction of asset valuations if and only if you're the only one with the efficiency, you're incentivized to keep it quiet.

If you're a nation state that's cracked a simple method to decrypt modern "pre-quantum" encryption schemes with less compute/wall time using a development in mathematics, it is in your interest to keep this quiet so that the parties you surveil to not switch or adapt. Similarly if you've figured out a handy new form of encryption, you're incentivized to prevent leaking of details as it is harder to reverse such operations without details of the methodology.

Or you've designed some special optimizer that you then bundle in a subscription service. Your business now only profits while the algorithm is secret. e.g. The DVD Copy Control Association's CSS encryption was only a valuable thing that the company could charge for or entice clients with before DeCSS was published/became popular.

There are different levels of outcomes, but even Terence Tao essentially foresees this issue: look at his remark footnote 5 in this very talk. It complements the Balkanization point in the parent comment. Not a big leap or unfathomable to connect to broader issues.

Update: see also the later slide where he problematizes corporate secrets in relation to math culture.

Everyone should just read the slides, really