I don't want to sound too disparaging here. Anyone who's ever seen my desk will know that I absolutely love pencils - they're so versatile that you can draw almost anything, and writing with a pencil is far more tactile than typing will ever be.
That said there are a bunch of problems with the way we do mathematics that we've all come across, but we just accept as a fact of life. I wan to propose that with the right software we could probably fix these.
The way we write mathematical working is usually just a long list of statements that follow directly from the previous. The first is trivial, the next follows from the first and so on.
The annoying thing about this, however, is that although there are often there are very small differences between the steps, you have to copy the whole thing out or it wouldn't make sense.
A simple solution to this problem is to LaTeX your maths work. LaTeX obviously has its own problems (don't get me started) but I will admit it is very easy to copy and paste.
Obviously LaTeX isn't going to be the solution to the rest of these problems.
All throughout my education career I've never been sure how much working I need to write. Examiners can be very difficult to guess. But contrast that with computer programming - I always know exactly how much 'working' the computer needs to run my program.
Can I use the result we proved in the previous maths exercise sheet? I don't know. We have to ask out teachers that all the time... But can I use the function I made previously? Well is it in scope? If so then I know I can use it, and it not I need to import or rewrite it.
If we get computers to help us with proofs, then the computer can keep track of what theorems are 'in scope' for us. There's no uncertainty! Perhaps teachers could provide a standard library that students are allowed to use - then if the computer thinks it's been proved with that library then it has been proved.
In school I loved it when teachers presented proofs of concepts as well as teaching them. But now that I'm studying Computer Science at university I'd really rather the professors kept the proofs to themselves. I very very rarely follow whole inductive proofs any more.
On reflection, while I would have alwalys asked for a proof, I don't think I ever really wanted proofs at school. I wanted intuition. The teacher never gave me an arbitary way to check that the statement was true, the teacher gave reasons why it makes sense that it would be true.
In a similar way when we teach algorithms courses, we know that showing code is never particularly helpful. Algorithms lecturers spend most of the time instead drawing boxes and lines to represent pointers and data structures and movments around them. These diagrams form the intuition, and then we can go home and program them on a computer on our own.
Likewise when teaching mathematical proofs, showing the actual proof is never particularly hepful. What we need is some diagrams with boxes with just enough intuition that we can go home and do the proof ourselves.
So if reading proofs doesn't help your understanding, then, as long as we have a way to verify proofs without reading them (i.e. by comptuer), there is no reason to read a proof!
Pencil and paper can never check a proof, so maths done on pencil and paper must be checked. The same goes for LaTeX, there's no way LaTeX can check a proof so the paper must be read and checked by a human.
But imagine the possibilities if we fully separated the disciplines of communicating intuition and doing proofs! We could actually fully check proofs, and we could make intuition so easy to understand.
I hope the possibilities of computer proof now look as exciting to you as they do to me.