Erdős problem 945
Is it true that ?
Sources
FormalConjectures/ErdosProblems/
945.lean
Retained formal statement
The two ways of phrasing the conjecture are equivalent.
Erdos945.Erdos945Prop ↔ Erdos945.Erdos945ConstantTextbookStatement only, no proof