Principia for Reverse Mathematics
If you've ever wondered about pure mathematics, metamath is an awesome site.

http://us.metamath.org/

It essentially is sort of like Principia Mathematica (Russel & Whitehead 1905) done right. It traces many features of mathematics down to fundamental axioms of set theory. Proof that there’s an unlimited number of primes? Its there. (A cool variation on the Euclid proof too that uses factorials instead of the normal resolution of impossible by assuming a highest prime) You can even prove that 2 + 2 = 4. Of course from the basics of set theory it takes 22607 steps...

But anyways I've wanted to contribute in some small way to metamath for a while. One of the things I'd like to do is formalize the generalized definition of exponentiation using Euler's identity. Its not there yet, and it is either the most beautiful or the most smartass equation in mathematics.

But I'm not totally familiar with the metamath language yet, and sort of constructing some basic proofs from ground zero right now, and having some trouble with it. I have some problems with metamath’s foundations.

First, I'm interested in constructive mathematics. Try to do math without assuming law of excluded middle or the axiom of choice, and if you can, throw away the axiom of infinity. I'm also interested in reverse mathematics. What axioms do you really have to assume to prove a theorem? So I wanted to start reconstructing the metamath project foundations with constructive set theory, and add additional axioms as ladders for doing math that absolutely requires it.

I'll start by just using a broader set of propositional calculus axioms (intuitionistic PC + double negation elimination) and trying to prove the Peirce's axiom, and if I get that far then the rest... well it won’t be easy but it will at least be something I can see finishing.

Okay, I'm sure most wont be the least bit interested in this, but I'm still excited about it.