Erdős problem 94 - regular ngon

Erdős and Fishburn also make the stronger conjecture that

\sum f(u_i)^2

is maximal for the regular

n

-gon (for large enough

n

$1,030 bounty

Solve it

Nobody has attempted this. A complete proof or refutation takes the whole bounty.

Submit a proof

Where this lives

conjectures-tasks

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

versions/fc-v2-variants-regular-ngon-1262dd5b80428331e33cbd39-formalized →

Formal statement

Proof target

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

namespace Bounty

theorem target : fcTypeOfName% "Erdos94.erdos_94.variants.regular_ngon" := by
  sorry

end Bounty

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

Original conjecture (Lean type)

∀ᶠ (n : ℕ) in Filter.atTop,
  ∀ (P : Finset (EuclideanSpace ℝ (Fin 2))),
    P.card = n →
      EuclideanGeometry.ConvexIndep ↑P →
        ∑ u ∈ distanceSet P, ↑(distanceMultiplicity P u) ^ 2 ≤
          ∑ u ∈ distanceSet (Erdos94.regularNGon n), ↑(distanceMultiplicity (Erdos94.regularNGon n) u) ^ 2

Original conjecture source: FormalConjectures/ErdosProblems/94.lean

The audit patch changes this file, so the upstream version can differ from the statement above.

Source type SHA-256: sha256:34addfb85c6d11514abbb657422db02276d5f6714e31453faab1e2340979a1a6
Task id: fc-v2-variants-regular-ngon-1262dd5b80428331e33cbd39-formalized
Task commitment: sha256:4df45980d46d398c68cfcff73c2fc7b15c3942093fb4a3163f59fb143a18ef53

References

erdosproblems.com/94

[Er92e] Erdős, Pál, Some Unsolved problems in Geometry, Number Theory and Combinatorics. Eureka (1992), 44-48.
[Er97c] Erdős, Paul, Some of my favorite problems and results. The mathematics of Paul Erdős, I (1997), 47-67.
[LeTh95] Lefmann, Hanno and Thiele, Torsten, Point sets with distinct distances. Combinatorica (1995), 379-408.

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

∀ᶠ (n : ℕ) in Filter.atTop, ∀ (P : Finset (EuclideanSpace ℝ (Fin 2))), P.card = n → EuclideanGeometry.ConvexIndep ↑P → ∑ u ∈ distanceSet P, ↑(distanceMultiplicity P u) ^ 2 ≤ ∑ u ∈ distanceSet (Erdos94.regularNGon n), ↑(distanceMultiplicity (Erdos94.regularNGon n) u) ^ 2