Skip to content

Erdős problem 1028

Start work

Let H(n)=min⁡fmax⁡X⊆{1,…,n}∣∑x<y∈Xf(x,y)∣,H(n)=\min_f \max_{X\subseteq \{1,\ldots,n\}} \left\lvert \sum_{x<y\in X} f(x,y)\right\rvert, where ff ranges over all functions f:{1,…,n}2→{−1,1}f:\{1,\ldots,n\}^2\to \{-1,1\}. Estimate H(n)H(n).

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/1028.lean

Formal Conjectures

FormalConjectures/ErdosProblems/1028.leanErdos1028.erdos_10281 lineExact file
(fun n => ↑(Erdos1028.H n)) =Θ[Filter.atTop] fun n => ↑n ^ (3 / 2)
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:1028
  • PLBY Lean proofsErdosProblems.Erdos1028

Reported activity

Reported by these sources. Not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry