Formalize Lennon–Pittel conjecture on the number of random stable matchings

### What is the conjecture

For each $n$, consider a balanced stable-marriage instance with $n$ men and $n$ women. Each of the $2n$ agents independently chooses a strict total ordering of the $n$ agents on the opposite side, uniformly among all $n!$ orderings.

A complete matching is a bijection between the men and women. It is stable if there is no unmatched man–woman pair such that both prefer one another to their assigned partners. Let $S_n$ be the number of stable complete matchings in the random preference profile.

The Lennon–Pittel conjecture states that, for every positive nonincreasing sequence $\varepsilon_n$ tending to zero,

$$
\Pr\left(S_n \geq \varepsilon_n\,\mathbb{E}[S_n]\right)
\longrightarrow 1
\qquad\text{as } n\to\infty.
$$

The explicit formulation appears in §1.2 and again as equation (6.0.1) of Craig Lennon's dissertation:

- Craig Lennon, *On the Likely Number of Stable Marriages*, Ph.D. dissertation, The Ohio State University (2007), advisor Boris Pittel.
https://etd.ohiolink.edu/acprod/odb_etd/ws/send_file/send?accession=osu1194991095&disposition=inline

The canonical published reference is:

- Craig Lennon and Boris Pittel, “On the Likely Number of Solutions for the Stable Marriage Problem,” *Combinatorics, Probability and Computing* 18(3) (2009), 371–421.
https://doi.org/10.1017/S0963548308009607

The conjecture appears to remain open. Preliminary searches found no later accepted proof or counterexample and no existing formalization in this repository, Mathlib, or other public Lean developments. I will repeat the status and duplicate checks before opening a pull request.

### Prerequisites needed

A minimal definition-only stable-marriage model is needed to state the conjecture:

- finite balanced preference profiles on `Fin n`;
- strict complete preference lists, represented as permutations assigning ranks;
- complete matchings represented as equivalences/bijections;
- blocking pairs and stability defined directly from the preference ranks;
- the number $S_n$ of stable complete matchings;
- the uniform PMF on the finite type of all preference profiles;
- the expectation of $S_n$ and the probability of the threshold event under that same distribution;
- positivity, antitonicity, and convergence to zero for $\varepsilon_n$;
- convergence of the event probability to $1$ along `atTop`.

The intended uniform distribution on the complete profile type gives exactly the joint law of $2n$ mutually independent uniform preference lists.

The reusable definitions would likely be placed in
`FormalConjecturesForMathlib/Combinatorics/StableMarriage.lean`, with the conjecture itself in
`FormalConjectures/Paper/LennonPittelStableMatchings.lean`.

No Gale–Shapley algorithm, structural stable-matching results, asymptotic estimates, or proof-oriented lemmas are planned.

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

* ams-05
* ams-60

### Choose either option

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