0 boosts
(PDF) Quine's New Foundations for set theory, in which the axiom of choice is false, has been formally proved in Lean to be consistent