Indeed, looks like scientific literature in general and mathematical literature in particular are stuck in the past century. As much as I enjoy reading printed materials, I often think that using a modern computer-based approach to presenting them could prove a lot superior. And no, PDF would not cut it, even with the possibility of hyperlinking. In my view, PDF is like the idea of the horseless carriage, or, rather, of a carriage pulled by a mechanical horse - a new technology stuck in the past. Looks like the modern web browser platform, on the other hand, could provide a reasonable base on which one could build an extremely powerful "IDE" for creating and interacting with mathematical expositions.
> Then how come an unfamiliar piece of source code is easier to follow than a mathematics paper using unfamiliar notation?
This is clearly subjective. I read lots of mathematics research that I find more accessible than even pretty mundane source code (and yes, I write software for a living and have done so for over ten years).
>
A mathematical formalism that could be interpreted in a purely mechanical way would be a huge improvement.
Look at Homotopy Type Theory:
I feel obliged to point out that HoTT is… really rather abstract. I'm just starting to learn about it now in my spare time, and I hold a master's degree in mathematics specialising in logic.
The answer to all of your questions: computer programs are written for computers to understand, and computers aren't very smart. Mathematical papers are written for mathematicians to understand, and they tend to be a lot smarter than computers.
Machine language is also written for computers to understand, but it's not easy to read. Computer-formalized math is usually even harder to read than regular notation. I don't think computers have much to do with this.
True, I should have said it better as, programming languages are written for compilers to read, and they're not very smart. Machine language is written for computers themselves. Computer-formalized math I don't think is written for anyone to read.
Then how come an unfamiliar piece of source code is easier to follow than a mathematics paper using unfamiliar notation?
You can look up the definition of each function and learn precisely what it does, without ambiguities. You can open up a debugger and trace every step of the algorithm. Source code tends to be formatted to emphasise its division into units that can be analysed separately. Even if the code uses a framework you don't recognise, you can probably understand some of the underlying logic just fine, thanks to a consistent syntax and (often) descriptive function names.
In a mathematical paper, often there's some notation that isn't defined and there isn't even any pointer where to look for definitions. Important objects are given one-letter names. Theorems are often only numbered; good luck remembering what lemma 2.17.3b was about. Proofs are written in prose (instead of something like Leslie Lamport proposed[0]). You have to fill in conceptual gaps and remind yourself of unstated assumptions. Notation and terminology is often ambiguous — what does "exponential time" mean? Is it DTIME(2^(c*n)) or DTIME(2^polynomial(n))? Does "increasing" mean "strictly increasing" or "non-decreasing"? Is zero a natural number? And so on.
A mathematical formalism that could be interpreted in a purely mechanical way would be a huge improvement.
[0] http://research.microsoft.com/en-us/um/people/lamport/pubs/p...