Erdős problem 82 · problems.science

$F(n) / \log n \to \infty as n \to \infty$

Sources

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

2 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

82.lean

Retained formal statement2 of 2

$F(n) \le O(n^{1/2} \ln ^ {3/4} n)$

Theorem 1.4 from [AKS07]

[AKS07] Alon, N. and Krivelevich, M. and Sudakov, B., Large nearly regular induced subgraphs. arXiv:0710.2106 (2007).

FormalConjectures/ErdosProblems/82.leanErdos82.erdos_82.variants.F_upper_bound1 lineExact file

1(fun n => ↑(Erdos82.F n)) =O[Filter.atTop] fun n => √↑n * Real.log ↑n ^ (3 / 4)

SolvedStatement only, no proof