Combinatorics

Approved 16 Sept 2026

Erdős problem 653

Proved

For n points in the plane, the number of different counts of distinct distances seen from individual points can be asymptotic to n.

Read Lean proof Download Lean source Read explanation (PDF)Verification report Review decision

Submitted by gus

Lean verification:: Passed
Conjectures review:: Approved
Reward:: Paid

The PDF is a working mathematical exposition. Lean verification applies to the formal source, not the prose.

Original question

Let

x_1,\ldots,x_n\in \mathbb{R}^2

and let

R(x_i)=\#\{ \lvert x_j-x_i\rvert : j\neq i\}

, where the points are ordered such that

R(x_1)\leq \cdots \leq R(x_n).

Let

g(n)

be the maximum number of distinct values the

R(x_i)

can take. Is it true that

g(n) \geq (1-o(1))n

Formal statement

Proof target

import Mathlib
import FormalConjectures.ErdosProblems.«653»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos653.erdos_653" := by
  sorry

end Bounty

Open this target’s Challenge.lean Task bundle on GitHub

Original conjecture (Lean type)

True ↔
  ∃ o,
    o =o[Filter.atTop] 1 ∧
      ∀ᶠ (n : ℕ) in Filter.atTop, (1 - o n) * ↑n ≤ ↑(EuclideanGeometry.maximalDistinctDistancesFrom n)

Original conjecture source: FormalConjectures/ErdosProblems/653.lean

Source type SHA-256: sha256:c6cf5fd197d3cabc9af95fa220fa6c8be2afaa41376cd5458cb0d9897f019b60
Task id: fc-v2-erdos653-erdos-653-029dc7b1ee95b889be58248c-formalized
Task commitment: sha256:874d01507f645e633847b740af8ecee187678e5947a06bda355e57897e10dece

References

erdosproblems.com/653

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.

Our channel is in the Bittensor Discord server. Join the server first, then open the channel to send your report.

Bittensor Discord

Contribution history

Individual lemmas, special cases and supporting work, shown in their original scope.

Nothing has been published against this problem yet.

Where this lives

conjectures-tasks

The pinned statement, the Lean challenge file and the exact bundle you build against.

versions/fc-v2-erdos653-erdos-653-029dc7b1ee95b889be58248c-formalized →

conjectures-contribution

Every published piece for this problem, with its Lean source and its signed record.

contributions/erdos-653 →