"I formalized the [board game Caverna] in Lean 4 and proved that my strategy is the unique weakly dominant pure strategy across every possible game configuration. My friends think this is excessive." https://www.stephendiehl.com/posts/caverna/