feat(ErdosProblems): 1088, Distinct Distances Conjecture in ℝᵈ #1386
Conversation
|
Thanks for your pull request! It looks like this may be your first contribution to a Google open source project. Before we can look at your pull request, you'll need to sign a Contributor License Agreement (CLA). View this failed invocation of the CLA check for more information. For the most up to date status, view the checks section at the bottom of the pull request. |
|
This PR adds Erdős Problem #1088, an open conjecture related to distinct distances among points in high-dimensional Euclidean space. The problem defines a function that measures the minimum number of points required so that any such set contains a subset of points where all pairwise distances are different. The conjecture asks for estimates of this function and whether it grows subexponentially with respect to the dimension when the number of points is fixed. Status: Open This contribution helps expand the repository’s coverage of open Erdős problems and makes this conjecture available for future discussion and exploration. |
YaelDillies
changed the title
| @[category research open, AMS 51] | ||
| theorem erdos_1088_general : | ||
| (∀ d ≥ 1, ∀ n ≥ 1, ∃ m, ∀ S : Finset (ℝ^d), S.card = m → hasSubsetWithDistinctDistances n S) | ||
| ↔ answer(sorry) := by | ||
| sorry | ||
|
|
||
| @[category research open, AMS 51] | ||
| theorem erdos_1088_exponential : |
There was a problem hiding this comment.
Can you please document both conjectures in latex?
YaelDillies
added
the
awaiting-author
2 participants
This PR adds Erdős Problem #1088, an open conjecture related to distinct distances among points in high-dimensional Euclidean space.
The problem defines a function that measures the minimum number of points required so that any such set contains a subset of points where all pairwise distances are different. The conjecture asks for estimates of this function and whether it grows subexponentially with respect to the dimension when the number of points is fixed.
Status: Open
Reference: https://www.erdosproblems.com/1088
This contribution helps expand the repository’s coverage of open Erdős problems and makes this conjecture available for future discussion and exploration.
Closes #1288