flâneur

abelianpi.dev/post/lean-prove-1080-sets

abelianpi.dev · 1,675 words · saved by 1 readers

All of my friends know that I play Set at a level so beyond obsessive it almost integer overflows to mundane -- the simplicity and symmetry of the game makes for an easy way to reset the marbles in my brain, and it's a quick way to idly pass by a minute or two between subway stops. Because of the elegant (one could even say algebraic) nature of the game, it's also fun to use for combinatorics questions. Since I've been trying to get more used to Lean anyway, I decided to try proving some Set combinatorics in Lean. Let's first look at how many distinct sets there should be from the deck of 81 cards. The Fundamental Theorem of Set says that given two cards, we can uniquely determine the third card in the set (try it!). So there are ( 81 2 ) ⋅ 1 3 = 1080 ( 2 81 ​ )⋅ 3 1 ​ =1080 unique sets we can create (remember we divide by 3 to correctly account for the 3 different ways to choose the first 2 cards from the 3 cards in a set). I won't go into the rules of Set or how I chose the spec

Using Lean to Prove 1080 Sets abelianpi understanding through writing Search On this page No sections yet 🔴 🟡 🟢 Using Lean to Prove 1080 Sets ← Back to Posts Using Lean to Prove 1080 Sets All of my friends know that I play Set at a level so beyond obsessive it almost integer overflows to mundane -- the simplicity and symmetry of the game makes for an easy way to reset the marbles in my brain, and it's a quick way to idly pass by a minute or two between subway stops. Because of the elegant (one could even say algebraic) nature of the game, it's also fun to use for combinatorics questions. Si

saved by

related reading