> I wonder if Russel & Whiteheads's classic 1+1 proof has yet been (computer-)formalized?

http://us.metamath.org/mpegif/pm54.43.html (though using a slightly different set of axioms to R&W: http://us.metamath.org/mpegif/mmset.html#axioms)