The big change will come more from natural language processing than from theorem-proving. There is already a huge corpus of carefully formalized mathematics that human mathematicians have been developing for hundreds if years. The only issue is the "carefully formalized" is by human standards and in natural human languages. Sometime in the not-too-distant future someone will make a natural language AI sophisticated enough to use this corpus as a scaffolding for "assisted" theorem proving, where the prover being assisted is a program generating completely formalized proofs and the assistance is coming from the natural-language AI parsing textbooks and journal articles. Once such a thing exists and is good enough to parse and formally verify standard graduate textbooks, there will quickly be a shift that all research mathematics should be written in a way that is acceptible to humans AND verifiable by such provers. Mathematicians would love the verified correctness, but the main thrust will remain that mathematics is by humans and for a human audience.
This assumes that advanced mathematics is currently written by humans for humans. Many proofs can be a trudge for even highly trained humans. The field should really be working on making formalisms more accessible. It would be fantastic if what you describe came about by first making maths more accessible/intuitive through more interactive and graphical representations. Maybe a lot of these 'algorithm visualizations' that get posted to HN is the first step.
