Skip to content

Erdős problem 757

Start work

What is the supremum of the set of admissible numbers?

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

757.lean

Retained formal statement2 of 3

The supremum is strictly larger than 1 / 2, which is proved in [GyLe95].

FormalConjectures/ErdosProblems/757.leanErdos757.erdos_757.variants.lowerBound1 lineExact file
∀ {A : Set ℝ}, 1 / 2 < sSup {c | Erdos757.IsAdmissible c}
SolvedStatement only, no proof