Green's Open Problems #87

### What is the conjecture
https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf#problem.87

Let $p(k)$ be the limit as $n \to \infty$ of the probability that a random permutation on $[n]$ preserves some set of size $k$. Is $p(k)$ a decreasing function of $k$? Is $p(k) = (C + o(1))k^{-\alpha}(\log k)^{-3/2}$ for some absolute constant $C$?

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-60

### Choose either option
- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

Read the linked Green's Open Problems PDF, specifically problem 87, and review the formal-conjectures repository's conventions for adding conjectures. The work is done when this conjecture has been added as a Lean formalization with the AMS-60 classification and the repository's checks pass.

Written by the indexing model from the issue text.