Alternative axiomatization of boolean algebras

Stream: mathlib4

[Antoine Chambert-Loir]

In #31924, I started formalizing alternative axiomatizations of boolean algebras, as proposed by Huntington and Robbins. Basically, a boolean algebra is a commutative additive semigroup with a negation, and one single additional relational axiom. Huntington proved in 1933 that his axiom,
(xᶜ + yᶜ)ᶜ + (xᶜ + y)ᶜ = x led to boolean algebras. Robbins's axiom, ((x + y)ᶜ + (x + yᶜ)ᶜ)ᶜ = x, is the dual of Huntington's, but it happened to be more difficult to prove that it also leads to boolean algebras, this was done in several steps (Winker, 1992; McLune, 1996) using automatic provers.

My formalization started initially out of fun, but the translation from mathematical paper to formalized proof ends up being a bit boring and I wonder whether this should land in mathlib or not.

[Bhavik Mehta]

My opinion is that this shouldn't be in mathlib unless there's some other application where making a boolean algebra via these axioms is easier. I proved Robbins' conjecture here https://github.com/leanprover-community/mathlib3/blob/90daf3c2173a1a9c3686c073a6af11609cef04fa/archive/robbins.lean#L444 4 years ago, and similarly to you felt it was a bit boring! But perhaps putting it in Archive makes sense