from Hacker News

Music for Axiom of Choice

by protez on 3/29/13, 4:43 AM with 1 comments

• by lifthrasiir on 3/29/13, 8:17 AM

  Metamath is marvelous. Its proof explorer [1] has some 18,000 theorems (and counting) that are ultimately derived (and proved) from a small set of axioms [2]. Just looking at the list of these theorems makes me dizzy.

  [1] http://us.metamath.org/mpegif/mmtheorems.html [2] http://us.metamath.org/mpegif/mmset.html#axioms