I do a lot of programming that uses mathematics. I designed the error recovery file format “par2”. I worked as a quantitative trader.
What do I want from math? To be able to search math results, understand them, and apply them. But academic mathematicians are so inwardly focused - as these authors so obviously are - that it does all of these badly! Search is still with words, not symbols and formulae. As for comprehension, many math papers are unreadable to those not in the cliche of mathematicians in that specialty. And even applied math papers don’t ship code or specify the operations explicitly.
I wanted to fix this and in 2013 I worked on formal proof. It makes symbol search and application easy. I found out that the tools had been usable for decades at that point. But mathematicians didn’t use them because they had that inward focus and didn’t give a damn about math consumers.
AI is enabling formal proof. It will carry mathematics into the computer age, which the field should have joined with every other industry in the 1970’s! I welcome it. Math will get used more and that is what the work was meant to achieve in the first place.