Corroborate

Claim in Erdős problems that formal-conjectures marks solved

A published paper or arXiv preprint answers the main question of Erdős Problem #655 (theorem erdos_655 in formal-conjectures) in full (proof, disproof, or the exact value asked for) with no hypotheses beyond the problem's own.

Problem as stated at github.com/google-deepmind/formal-conjectures/blob/34ee0e3c5fd52d202d62a71094a37970cb5fb870/FormalConjectures/ErdosProblems/655.lean. The claim text is written by Corroborate; that site has not reviewed or endorsed it.

The problem, as stated in formal-conjectures (Apache 2.0):

Let x_1,\ldots,x_n\in \mathbb{R}^2 be such that no circle whose centre is one of the x_i contains three other points. Are there at least (1+c)\frac{n}{2} distinct distances determined between the x_i, for some constant c>0 and all n sufficiently large? The answer is **no**: as Zach Hunter observed, the regular `n`-gon (`n` points equally spaced on a circle) is valid and determines only `⌊n/2⌋ < (1+c)n/2` distinct distances, for every `c > 0`. (In the spirit of related conjectures of Erdős and others, presumably some kind of assumption that the points are in general position was intended; see `erdos_655.variants.general_position`.) The disproof — the regular `n`-gon construction together with its supporting lemmas — is formalised at the linked commit.

Verdict: no verdict yet

formal-conjectures marks problem #655 as solved. Those pages say who settled it and how.

Evidence for

None yet.

Evidence against

None yet.