That way, when people look at some mathy thing, they're not stuck wondering "what does that crazy looking symbol mean?" with no way of looking it up.
Also, if someone is not sure what a formula means, or isn't convinced that it is true, they can inspect the proof-program to understand it better.
I feel like this would make math less opaque, and more accessible to a wider audience.
Q: Don't you just mean that it would be more accessible to an audience of people like you, who know how to program?
A: Well, sortof. But with an open source program, I feel like an ambitious person can, in principle, figure out what is going on, as long as they understand the programming language in use (where the programming language itself tends to be relatively small, and well documented). All the information they need is there. But with a math paper that someone writes and publishes, it may be theoretically impossible for someone to understand without happening to have taken some class or read some book that explains some of the crazy symbols and shortcut notations.