On: New Foundations is consistent – a difficult mathematical proof proved using Lean

[klyrs]

> The number three is the set of all sets with three elements

I can't make up my mind if this is extremely elegant, or mindbogglingly horrendous; awesome or awful. I lean towards elegant, because the mindboggle caused by traditional set theory.

[randallholmes → klyrs]

I think the Frege definition of the natural numbers is philosophically the correct one. This is a point in favor of foundations in NFU. I also think that Zermelo-style foundations are pragmatically better, so sadly I must let go of the first preference :-)