There is a lot of work done towards formalizing existing proofs into logic software and proof wikis. The formalization of a proof can be very helpful economically. It can lead to more confidence in proofs and making searching for results more feasible.
(Mario here:) I am an undergraduate who works with the program and library Metamath for doing formal proofs. There is a TON of work that still needs to be done in formalizing even just the standard undergraduate curriculum, and it's all easily accessible to any reasonably bright undergraduate. It helps to be good at programming or at least thinking like a programmer, since the work you do looks a lot like programming to the uninitiated and formal math is just as unforgiving to typos as any compiler. But even though there is a lot of general problem solving involved, the path is all more or less written out by other mathematicians (as "hand proofs"), so the way forward is always clearly delineated and it might even be ungraciously called "transcription".
I'm going to try to keep it up in graduate school, but even just as a pastime it's good for the brain and gives you a great sense of accomplishment, in addition to making you understand the corresponding hand proof on a deeper level than pretty much any kind of study out there. It's not for the faint of heart, but for precision-minded amateur or professional mathematicians with a programming bent I could not recommend it enough.
