-
Notifications
You must be signed in to change notification settings - Fork 209
Description
What is the conjecture
Let
Conjecture: There exists a universal constant
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:
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
EquivandFintype) - 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
- ams-05
- ams-60
- ams-90
Choose either option
- 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
This issue was generated by an AI agent and reviewed by me.
See more information here: link
Feedback on mistakes/hallucinations: link