In the future, I hope, there will be more convergence between formal proofs systems and the mathematical notation for learning, teaching, and storing knowledge.

In the future, I hope, there will be more convergence between formal proofs systems and the mathematical notation for learning, teaching, and storing knowledge. Systems like Lean, Coq, Sage Math, Octave, etc should work together on bringing more uniformity to the representation. Not for the actual code or an engine but some uniform language/format/interface, bringing the way to read and write it as a daily math, while preserving portability between those systems.