Erdős problem 1097
The main conjecture: for any finite set of integers with , the number of distinct common differences in three-term arithmetic progressions is .
Sources
FormalConjectures/ErdosProblems/
1097.lean
Retained formal statement
A weaker bound has been proven: there are always at most such values of .
∀ (A : Finset ℤ), (Erdos1097.CommonDifferencesThreeTermAP A).ncard ≤ A.card ^ 2TextbookStatement only, no proof