In the first four-and-something months of 2024 I once again devoted myself to mathematics and the Lean theorem prover, getting a few PRs merged and doing some research on the number of "generalised bridge deals with specific voids". In the latter pursuit I discovered a seemingly simple combinatorial identity that in the end had to be proved by cutting-edge software from RISC-JKU.

I delved so deep that I harboured a genuine fear of losing my links to ponies and furries, for many years my deep-seated passion. But I was safe – my interest in mathlib4 was waning in the wake of the Lean FRO's establishment and the subsequent avalanche of new contributors, while I never had any reason to continue answering questions (aka "reputation farming") on the Mathematics Stack Exchange. Finally I bought my first two commissions from others in over six months and returned to complete this picture, my love letter to the Lean community.