(No, not what you think.)
For work today, I had to proofread some lecture notes for my boss. After work, I started wondering: What if we could leave the tedious verification of our math to computers? To me, math is about understanding and constructing, and not so much about meticulously verifying “old” proofs—an activity that I believe should be automated.
Coq is one system that achieves this, even though it’s geared more towards constructing rather than checking proofs. It’s written in Objective Caml and will be consuming a bit of my research time to come.
As an aside: While surfing the web surrounding Coq’s site, I discovered AEI’s Living Reviews, with that being journals of review articles that come with a promise of maintenance and actuality. Currently, this kind of journal only exists for solar physics and relativity. While the “current” system of just republishing an old review article is not bad, I think that making the whole maintenance process explicit and giving it a shorter turnaround time is actually a pretty good idea.