I definitely think that for mathematics, we'll have tools similar to chess engines (something like Lichess UI would be amazing) but to help us solve problems (well, this exists already, but it's not really that good, and the ambiguity it can tolerate is mostly hard coded stuff).

I heard a few months ago about a tool that transformed formal prover code into LaTeX (or vice-versa, I can't remember), based on GPT-3. I can't imagine this kind of tools not being a huge thing in the next few years. Especially, I'm expecting that future math articles will have code with formal proofs in appendix (or like a github link).