Erdős Problem #92
The statement as posed is false.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
For a given point `x` and a set of other points, this function finds the maximum number of points that lie on a single circle centered at `x`. It does this by grouping the other points by their distance to `x` and finding the size of the largest group.
This property holds for a set of points `A` if every point `x` in `A` has at least `k` other points from `A` that are equidistant from `x`.
The set of all possible values `k` for which there exists a set of `n` points satisfying the `hasMinEquidistantProperty k`. The function `f(n)` will be the supremum of this set.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · 2 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/92.Attempts
submit one →If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.