Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Problem 539
claims/: The 3 claim pages of Problem 539, one per claimant's result; the problem's standing derives from them.
Statement. Let be such that, for any set of size , the set
has size at least . Estimate .
Formulation. The site's wording (page last edited 15 June 2026). is the least, over sets of positive integers, of the number of distinct ratios with (the pair contributes the ratio ). Erdős's 1973 wording defines as the greatest integer such that any integers give at least distinct ratios , the same quantity, and asks to improve his bounds (5.2) and to determine . Granville and Roesler ask, for each , for the least number of integers in over sets of distinct positive integers (their Unsolved problem), and restate it for vectors: with the exponent vector of , the ratio has exponent vector , so is the least over -sets of vectors with nonnegative integer entries. The formal-conjectures file lets range over finite subsets of including and reads "estimate" as the order of growth . The site's source key is [Er73, p. 125]; it tags the page additive combinatorics and number theory.
Status. The site's label is OPEN. The refereed bounds are : the lower bound is Erdős and Szemerédi's, by the pairing argument Granville and Roesler give on p. 2 of their paper, and the upper bound comes from the Freiman–Lev sets in two dimensions, which Granville and Roesler present (pp. 2--3) and record as their Theorem 2; the accepted partial claim Granville and Roesler 1999 records both, on the refereed publication alone. Erdős's 1973 announcement of the bounds (5.2) with Szemerédi has no claim page: it gives no proof and no reference, and its content is carried by the Granville–Roesler page, which credits it. Two further partial claims have pages. The exponent: Theorem A.1 of the arXiv preprint of July 2026 by Schmitt, Gehrunger, Dekoninck, Bérczi, Kreitner, Price and Holmes describing their system ProofCouncil, to which they attribute it, gives , hence ; the site's curator, Thomas Bloom, adopted the bound into the commentary on 15 June 2026 after sketching the construction himself, while the label stayed OPEN, and its claim page records it as a pending partial claim (not refereed; the adoption of a bound into the commentary of a problem the site labels OPEN is not an acceptance, and nothing is reviewed by this project). The lower bound: a Lean development of September 2026 states that , read as neither built nor audited by this corpus, on [[problems/integer_sequences/E0539/claims/2026_09_05_kitamura|Kitamura's claim page]] (claimed). The authors of the exponent result write that the exact order of remains open within a subexponential factor, and this page reads the label OPEN the same way: the question asks for an estimate, and the order is not determined. No full claim exists, and the standing derives from the claim pages.
Source. erdosproblems.com/539, accessed 2026-09-18: the problem page (OPEN, with the site's note that no finite computation can settle it; last edited 15 June 2026; source key [Er73, p. 125]; commentary citing [GrRo99] and thanking two contributors), its eight-comment discussion thread (19 August 2025 to 15 June 2026) and its empty proof-claim tab, all three unchanged on 2026-10-07. Cite as: T. F. Bloom, Erdős Problem #539, https://www.erdosproblems.com/539, accessed 2026-09-18.
References.
- [GrRo99] Granville, A. and Roesler, F., The set of differences of a given set. Amer. Math. Monthly 106 (1999), no. 4, 338--344, DOI 10.1080/00029890.1999.12005050. The Unsolved problem, its restatement and the lower bound , p. 2; Theorem 1, p. 2; the Freiman–Lev sets and Theorem 2, pp. 2--3; the page numbers are those of the authors' eight-page preprint, public at https://dms.umontreal.ca/~andrew/PDF/Roesler.pdf, whose labels the journal version may not share. Library home: granville_1999_set_differences_given_set; result pages unsolved_problem, theorem_1, theorem_2.
- [Er73] Erdős, P., Problems and results on combinatorial number theory. A Survey of Combinatorial Theory (Fort Collins 1971), North-Holland (1973), Chapter 12, 117--138; Section 5, printed pp. 124--125; the chapter is online at https://www.renyi.hu/~p_erdos/1973-21.pdf. Library home: erdos_1973_problems_results_combinatorial_number_theory; result page section_5_h_n.
- [SGD+26] Schmitt, J., Gehrunger, T., Dekoninck, J., Bérczi, G., Kreitner, U., Price, L. and Holmes, D., ProofCouncil: An LLM Agent for Solving Open Mathematical Problems. arXiv:2607.09474v1 (10 July 2026, 25 pages; the paper describes the authors' system ProofCouncil, which the site's commentary names). Appendix A, "Case Study: Erdős Problem 539", pp. 10--15: Theorem A.1, p. 11; the proof, pp. 11--14; the scope of its Lean development, p. 15. Not carded in the library.
- [HLP08] Holzman, R., Lev, V. F. and Pinchasi, R., Projecting difference sets on the positive orthant. Combin. Probab. Comput. 17 (2008), no. 5, 681--688. Not held; its fixed-dimension lower bounds are quoted from the thread and from [SGD+26].
- Freiman and Lev: the two-dimensional construction credited to them by [GrRo99] (pp. 2--3), which gives no reference for it; nothing of theirs is held.
- The external Lean developments named by the formal-conjectures file:
KitaKen1/erdos-539-formal-conjectures(commit of 11 August 2026) andKitaKen1/erdos-539-sqrt-disproof(commit of 5 September 2026), pinned on the claim pages; not library sources.
Formalization. Statement only. The file
ErdosProblems/539.lean
of formal-conjectures, at the pinned commit of its main branch as of 2026-09-18,
defines cofactorThreshold n as the largest m such that every n-element
Finset ℕ has at least m values a / a.gcd b, and declares erdos_539 : (fun n ↦ (cofactorThreshold n : ℝ)) =Θ[atTop] (answer(sorry) : ℕ → ℝ) under
category research open with proof sorry. Its variants, all research solved
and sorry, record (no attribute), (no
attribute), the negative answers to and
(with formal_proof attributes naming lines of lean/Erdos539SqrtFC.lean in
the second repository above), the negative answers to and
and the limit Tendsto (fun n ↦ Real.log (cofactorThreshold n) / Real.log n) atTop (nhds (1/2)) (with attributes naming lines of
lean/Erdos539/FC.lean in the first repository), citing Theorem A.1 of [SGD+26]
in their docstrings. The community database, records the problem open (record
last updated 31 August 2025), the statement formalized since 16 April 2026 and
no formal proof. The site's page marks the statement as formalized. Nothing was
built or audited by this corpus. The two external repositories are described
below.
Current assessment
The question (site formulation as of 2026-09-18). The statement above; OPEN; last edited 15 June 2026. The commentary, in this page's words: Erdős and Szemerédi proved for some ; Freiman and Lev improved the upper bound to ; both proofs are in the paper of Granville and Roesler [GrRo99], who also recast the problem in combinatorial geometry through the vectors with coordinates , from which they drew lower bounds beating when the dimension is a fixed small number; and, in the same form, ProofCouncil, the system the commentary names, proved , so . The thread, oldest first: 19 August 2025, the bounds from [GrRo99], with the lower bound attributed, tentatively, to Erdős and Szemerédi and the upper bound credited by the paper's authors to Freiman and Lev, and the fixed-prime-set results , , of [GrRo99] and [HLP08] (the site was updated); 22 May 2026, a conjectured formula , , fitted to those three exponents, with its author's later retraction of the heuristic behind it and a note that Holzman, Lev and Pinchasi speculate for all instead; 10 June 2026, the announcement of the exponent result by an account of one of its authors; 11 June 2026, a question where the proof is and two replies, one locating it in the paper's Appendix A.1 and one reporting a check that found no issue in the informal proof and two reservations, that the accompanying Lean formalization proves only the exponent limit and that the unpublished Bollobás–Leader announcement (below) is a risk to novelty; 12 June 2026, a comparison of the new fixed-dimensional exponents with the fitted formula; and 15 June 2026, the site's curator's simplified sketch of the construction (below). The proof-claim tab is empty. The claims are on the pages of the exponent result and of [[problems/integer_sequences/E0539/claims/2026_09_05_kitamura|the square-root development]].
Origin (Er73, printed pp. 124--125). Section 5 opens with Graham's problem (5.1), for integers , Szemerédi's proof for prime, Winterle's for prime, and the theorem of Marica and Schönheim that squarefree 's give at least distinct ratios . Then (p. 125): "Denote by the greatest integer so that there are at least distinct ratios of the form (5.1). Szemerédi and I showed
It would be interesting to improve (5.2). The determination of will perhaps not be too difficult." No proof is given there; the site's is (5.2). The announcement has no claim page: the chapter is a proceedings survey that proves nothing and cites nothing for (5.2), and the bounds entered the literature with proofs through [GrRo99], whose claim page credits Erdős and Szemerédi for the lower bound.
The refereed bounds (Granville and Roesler). The Unsolved problem (p. 2) is the site's question for each , with the restatement for vectors and the lower bound: for fixed the pairs , , are distinct because , so one of the two coordinate sets has at least values, giving . The paper gives this argument without attribution; the site and Erdős credit the bound to Erdős and Szemerédi, and the paper credits the sets behind the upper bound to Freiman and Lev. Theorem 1 (p. 2): for of distinct vectors, has at least vectors, so sets built from two primes give at least ratios; the Freiman–Lev sets with have , so the exponent is right in the plane up to the factor (pp. 2--3). Theorem 2 (p. 3) collects the two: if is minimal over -sets then , that is ; these two bounds are the accepted partial claim Granville and Roesler 1999, accepted on the refereed publication alone. Read depth: claims checked for the three statements and the pairing argument; the proof of Theorem 1 (p. 4) is not checked. The paper's Theorems 3 and 4, on the symmetric quantity , are a different problem and are not used by this corpus. The fixed-dimension bounds of [HLP08] quoted in the thread ( for three primes, for four) are second-hand.
The 2026 upper bound (a pending partial claim; see its claim page). Theorem A.1 of [SGD+26] (p. 11), stated for over sets of positive integers: there is an absolute constant such that for every
and consequently . The proof (pp. 11--14) passes to the vector form (Lemma A.2, the equivalence over all dimensions), takes a two-dimensional strip with and (Lemma A.5), applies a "separated suspension" with and (Lemma A.6), iterates it times to get exponents in dimension (Propositions A.7 and A.8), and lets grow with ; the lower bound is Proposition A.4, from (Lemma A.3) and . The site's author's sketch of 15 June 2026 gives the same construction from by the recursion , with and the choice , . Provenance and standing, as the paper gives them: Appendix A.1 "is a cleaned-up example output" of the system; the authors present the result as a partial solution, "verified by human experts"; the accompanying Lean development (Section A.2) proves, in the authors' description, the universal lower bound, upper bounds with explicit constants for each fixed suspension depth, and the exponent conclusion of Theorem A.1, while the sharper explicit upper bound is, they write, established at present only by the informal proof; and the authors record that Bollobás and Leader "previously announced a negative answer to the question" in seminar abstracts of 2009 and 2012 (Warwick; Oxford), that they know of no written account of that work, and "make no claim of priority over that announcement". The site adopted the bound into its commentary on 15 June 2026. No refereed publication, arXiv version of the appendix as a separate paper, or independent review was found; the two thread reservations of 11 June 2026 are recorded above. Read depth: claims checked for Theorem A.1 and the lemma statements; the three-page proof is checked for its structure only, not step by step; nothing is independently reviewed by this project. The claim page named under Status records the curator's adoption of the bound and why it is not an acceptance.
The two Lean developments. Two repositories named by the
formal-conjectures file are pinned on the claim pages; neither was built or
audited by this corpus. KitaKen1/erdos-539-formal-conjectures
(commit of 11 August 2026): its lean/Erdos539/FC.lean bridges the
collection's zero-inclusive definition to the positive-integer definition of
the paper's Lean development (which it imports at a pinned commit of the
system's own repository, per its README) and proves the exponent limit and
the negative answers to the variants; its README says the bridge
and resolution proofs were developed with assistance from OpenAI Codex.
KitaKen1/erdos-539-sqrt-disproof (commit of 5 September 2026): its
lean/Erdos539SqrtFC.lean states threshold_div_sqrt_tendsto, that
for the collection's cofactorThreshold, without
hypotheses, and derives the
negative answers to and ; its README
describes the argument as a weak form of the polynomial Freiman–Ruzsa
theorem, vendored from the teorth/pfr project, combined with an
induction on dimension, and discloses that OpenAI Codex assisted with the
proof development, formalization and exposition (the README revision of the
same day at the repository's head names it as OpenAI Codex (GPT-6 Astra)).
If sound, the second development shows that the Erdős–Szemerédi lower bound
is not sharp in order, which the site's commentary does not
record and which no paper states; it has its own claim page,
named under Status, as a pending partial claim. The lakefile of the first
repository names Kenta Kitamura as copyright holder. The collection's own
file carries the
negative answers as research solved variants with sorry bodies.
Search scope. None of the routes below found a refereed determination of the order of , a refereed version of the 2026 appendix, or an independent review of it.
- The site: problem page, discussion thread and proof-claim tab; the formal-conjectures file at the pinned commit; the community database as of that date.
- arXiv: the abstract page of 2607.09474 (one version, 10 July 2026; the
listing's comment says that ProofCouncil took part as System A in a
challenge report, arXiv:2606.18119, not consulted) and its PDF; the API
queries for the name ProofCouncil (one record, the
preprint) and
abs:"Erdős problem" AND (abs:535 OR abs:536 OR abs:538 OR abs:539)(no records; titles and abstracts only). - GitHub: the two repositories above (commit dates, the two Lean files, the two READMEs and lakefiles).
- The primary sources: [GrRo99] pp. 1--3; [Er73] pp. 124--125; [SGD+26] pp. 9--15.
- On 2026-10-07: the site's page, thread and proof-claim tab were unchanged, and the arXiv listing of 2607.09474 had one version.
Not searched: MathSciNet, zbMATH, Google Scholar, X; the seminar abstracts of 2009 and 2012 cited by [SGD+26]; the challenge report arXiv:2606.18119. Not held: [HLP08], the Freiman–Lev source. Not checked: the proof of Theorem 1 of [GrRo99] (p. 4).
Remaining gaps. (1) The order of is open within the factor ; the exponent rests on an unrefereed appendix attributed to ProofCouncil, a pending partial claim adopted into the site's commentary under the label OPEN and reviewed by nobody of this corpus; being partial, it would leave the standing open in any case. (2) The claim exists only as a Lean development, not built or audited by this corpus, a pending partial claim. (3) The Bollobás–Leader announcement has no written account. (4) Proof coverage is at statement level throughout; Theorem 1 of [GrRo99] is compiled without its proof.
Linked library material
These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.
- erdos_1973_problems_results_combinatorial_number_theory
- erdos_1973_problems_results_combinatorial_number_theory / section_5_h_n
- granville_1999_set_differences_given_set
- granville_1999_set_differences_given_set / theorem_1
- granville_1999_set_differences_given_set / theorem_2
- granville_1999_set_differences_given_set / theorem_3
- granville_1999_set_differences_given_set / theorem_4
- granville_1999_set_differences_given_set / unsolved_problem