Erdős problem 757
What is the supremum of the set of admissible numbers?
Sources
FormalConjectures/ErdosProblems/
757.lean
Retained formal statement
The supremum is strictly larger than 1 / 2, which is proved in [GyLe95].
∀ {A : Set ℝ}, 1 / 2 < sSup {c | Erdos757.IsAdmissible c}SolvedStatement only, no proof