The real Mizar asset is a growing collection of proofs written in a machinable format. There are at least informal understandings of these proofs and I can think of nothing better than several projects to produce programs to read these proofs and provide their own judgements. Some of these programs might mechanically transform some of the proofs into proofs in simpler logic systems. Such transforms would generally be expansions. Other transformations might go the other way, but that’s harder

It would be nice to know which theorems rely on the axiom of choice, the continuum hypothesis, or even the law of the excluded middle. I remember being recently terrified when I learned that AC was necessary to show that the union of a denumerable number of denumerable sets was denumerable.

As I took courses in formal logic I slowly came to believe that such logic sufficed for the math that I was otherwise interested in. Such is the inspiration behind Mizar.

Relates to: this, & this

Robbins conjecture + is or 0011 x 0101 y 1100 n(x) 1101 n(x) + y 0010 n(n(x) + y) 1010 n(y) 1110 n(x) + n(y) 0001 n(n(x) + n(y)) 0011 n(n(x) + y) + n(n(x) + n(y)) which is x.