Mathlib

Start with a set and a binary operation. Demand associativity, a unit, and inverses.