> I wonder if Russel & Whiteheads's classic 1+1 proof has yet been (computer-)formalized? http://us.metamath.org/mpegif/pm54.43.html http://us.metamath.org/mpe

> I wonder if Russel & Whiteheads's classic 1+1 proof has yet been (computer-)formalized? http://us.metamath.org/mpegif/pm54.43.html 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 http://us.metamath.org/mpegif/mmset.html#axioms)