I was puzzling: "What is the shortest proof of $\exists x \forall y (P(x) \to P(y)) $?" (a variation of the drinkers paradox see Proof of Drinker paradox) given a certain set of inference rules and using natural deduction.
I managed to proof it in 23 lines, but I am not sure if this is the shortest possible proof.
That made me think maybe I could turn it into a little competition and offer say 200 reputation as reward for the shortest proof.
Would such a (competition) question be allowed?