Talagrands Matching Conjecture

### What is the conjecture

Let $N$ be a positive integer. Consider two independent sequences $(X_i)_{i=1}^N$ and $(Y_i)_{i=1}^N$ of points uniformly distributed in $[0,1]^2$, where $X_i = (X_i^1, X_i^2)$ and $Y_i = (Y_i^1, Y_i^2)$.

**Conjecture:** There exists a universal constant $L > 0$ such that for any $\alpha_1, \alpha_2 > 0$ satisfying $\frac{1}{\alpha_1} + \frac{1}{\alpha_2} = \frac{1}{2}$, with probability at least $\frac{1}{2}$, there exists a matching $\pi \in S_N$ (permutation of $\{1, \ldots, N\}$) satisfying:
$$\sum_{i=1}^N \exp(\alpha_1 |X_i^1 - Y_{\pi(i)}^1|) \leq 2N \quad \text{and} \quad \sum_{i=1}^N \exp(\alpha_2 |X_i^2 - Y_{\pi(i)}^2|) \leq 2N.$$

**Specific cases of interest:**
- When $\alpha_1 = \infty$ and $\alpha_2 = 2$: The matching satisfies $\max_{i=1}^N |X_i^1 - Y_{\pi(i)}^1| \leq L\frac{\sqrt{\log N}}{\sqrt{N}}$.
- When $\alpha_1 = \alpha_2 = 4$: The matching satisfies $\sum_{i=1}^N |X_i - Y_{\pi(i)}|^2 \leq L\frac{(\log N)^{3/2}}{\sqrt{N}}$ where $|\cdot|$ is Euclidean distance.

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

A proof is worth 1000$.

**Sources:**
- https://michel.talagrand.net/prizes/matchings.tex

### Prerequisites needed

**Formalizability Rating:** 4/5 (0 is best) (as of 2026-01-22)

Building blocks (1-3; from search results):
- Permutations and matchings as bijections on finite sets (available in Mathlib via `Equiv` and `Fintype`)
- Real exponential function and basic analysis (available in Mathlib)
- Probability and measure theory (foundational concepts in Mathlib via `Measure`)

Missing pieces (exactly 2; unclear/absent from search results):
- Formalization of uniform random point distributions on $[0,1]^2$ and joint independence of two sequences
- Definitions of optimal matching costs with exponential moment constraints and related probability concentration bounds

Rating justification (1-2 sentences): The core combinatorial and real-analytic concepts (permutations, exponential bounds) are available in Mathlib, but formalizing this conjecture requires building substantial probabilistic infrastructure around independent uniform distributions and matching cost measures. This is significant new theory rather than routine definitions.

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

* ams-05
* ams-60
* ams-90

### 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

---
This issue was generated by an AI agent and reviewed by me.

See more information here: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)

Feedback on mistakes/hallucinations: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Issue.20Agent.20Feedback.20Topic/with/569223911)

No repository file, test, or entry point is named. Start by reading the linked Talagrand source and checking the stated Mathlib building blocks, then determine the missing probability and matching infrastructure. Done would mean adding the conjecture to the Lean repository with the required definitions and formal statement.

Written by the indexing model from the issue text.