Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Claim. The answer to Problem 1185 is no, already for : there are and, for every , arbitrarily large with sets , and , such that no nontrivial -term arithmetic progression in has its common difference in . The claimed input is the example in H. Furstenberg, Recurrence in ergodic theory and combinatorial number theory (M. B. Porter Lectures, Princeton University Press, 1981), pp. 177--178: an infinite set whose difference set is a set of recurrence but not a set of -recurrence. Call -intersective if every set of positive upper density contains a -term arithmetic progression with difference in ; by Furstenberg's correspondence principle a set of -recurrence is the same as a -intersective set, so there is a set of positive upper density with no -term progression whose difference lies in . Given , let be the smallest elements of ; for infinitely many the set has at least elements, $B\subseteq {1,\ldots,N}$, and meets no difference of a -term progression in . This is the deduction the site's commentary records and the page restates in its own words; since a -term progression contains a -term progression with the same difference, the same and refute the question for every . Erdős and Mauldin asked it as a question, motivated by a problem in measure theory ([Er80], p. 92, on the card erdos_1980_survey_problems_combinatorial_number_theory); its answer is no, so the claim is a disproof. Frantzikinakis, Lesigne and Wierdl (Ann. Inst. Fourier 56 (2006), 839--849, arXiv:math/0503367) locate Furstenberg's example on those pages and extend it to a set of -recurrence that is not a set of -recurrence for every ; their explicit sets (, irrational; their Theorem A) are not presented as difference sets, and Furstenberg's example alone already answers the question no for every , so they are context here. The DOI linked above is the publisher's record of the book.
Formalization. Boris Alexeev's lean-proofs repository holds, since
2026-08-17, a Lean 4 development that declares itself a formalization of a
solution, with Furstenberg as its informal author and Codex and GPT-5.6 Sol as
its formal authors (src/latest/ErdosProblems/Erdos1185.lean, linked above at
the pinned commit). Its theorem not_erdos_1185 shows that the universal
statement fails at and : for every proposed and every
cutoff there are beyond the cutoff and sets
with and and no nontrivial
-term progression in with difference in , built from a finite
periodic form of Furstenberg's quadratic skew-shift example. This corpus has
not built it, so no formalized evidence is listed.
Depends on. Nothing in this wiki.
Acceptance. Reviewed: the site's curator, Thomas Bloom, labels the problem solved, states that it is false already at , and credits Furstenberg's example [Fu81] for the infinite set whose difference set is not -intersective (page last edited 5 April 2026; empty discussion thread and proof-claims tab); he is independent of Furstenberg, and the deduction from the example to the finite statement is his own commentary. Not refereed: the source is a published monograph, not a journal article, and the deduction from it to the finite statement appears only in the site's commentary; the 2006 Annales paper that cites the example is refereed but is not the source of the claim. The example's property is stated as the commentary and the 2006 paper give it.