Erdős problem 1028 · problems.science

Let $H(n)=\min_f \max_{X\subseteq \{1,\ldots,n\}} \left\lvert \sum_{x<y\in X} f(x,y)\right\rvert,$ where $f$ ranges over all functions $f:\{1,\ldots,n\}^2\to \{-1,1\}$ . Estimate $H(n)$ .

Sources

Browse retained paths and inspect the exact material available for this Problem.

4 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1028.lean

Retained formal statement1 of 4

Let $H(n)=\min_f \max_{X\subseteq \{1,\ldots,n\}} \left\lvert \sum_{x<y\in X} f(x,y)\right\rvert,$ where $f$ ranges over all functions $f:\{1,\ldots,n\}^2\to \{-1,1\}$ . Estimate $H(n)$ .

Erdős [Er63d] proved $\frac{n}{4}\leq H(n) \ll n^{3/2}.$ Erdős and Spencer [ErSp71] proved that $H(n)\gg n^{3/2}$ .

FormalConjectures/ErdosProblems/1028.leanErdos1028.erdos_10281 lineExact file

1(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.

Sources

Search problems.science