Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated Oct 8

Problem 164

claims/: The 2 claim pages of Problem 164, one per claimant's result; the problem's standing derives from them.

Statement. A set $A\subset \mathbb{N}$ is primitive if no member of $A$ divides another. Is the sum

\sum_{n\in A}\frac{1}{n\log n}

maximised over all primitive sets when $A$ is the set of primes?

Status. PROVED (LEAN).

Source. erdosproblems.com/164, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #164, https://www.erdosproblems.com/164.

References.

[ABLLPSTT26] B. Alexeev, K. Barreto, Y. Li, J. D. Lichtman, L. Price, J. I. Shah, Q. Tang, and T. Tao, Primitive sets and Von Mangoldt Chains: Erdős problem #1196 and beyond. arXiv:2605.00301 (2026).
[Er35] Erdős, Paul, Note on Sequences of Integers No One of Which is Divisible By Any Other. J. London Math. Soc. (1935), 126-128.
[Li23] Lichtman, J. D., A proof of the Erdős primitive set conjecture. arXiv:2202.02384 (2023).

Formalization. Statement in formal-conjectures.

Current assessment

The site's formulation (accessed 2026-09-04; the site's page was last edited 2026-05-12) asks whether $\sum_{n\in A}1/(n\log n)$ over primitive sets $A$ is largest when $A$ is the set of primes. The answer is yes, and the standing derives from two accepted full claims: Lichtman 2022, the first proof, refereed in Forum of Mathematics, Pi in 2023 and credited by the site's curator, and Alexeev and coauthors 2026, a shorter proof by Markov chains with von Mangoldt weights, a preprint the curator credits as an alternative proof. Erdős proved in 1935 that the sum converges for every primitive set. Lichtman's paper also shows every odd prime is Erdős strong, and the second paper settles the prime $2$ . The same second paper addresses the related problems Problem 1196 and Problem 1217.

The site's label carries a Lean qualification: the formal-conjectures statement file names as its formal proof a Lean file in Boris Alexeev's repository, which formalizes a variant of the second proof and is linked from that claim page. The file is third-party Lean that this corpus has not built, so neither claim lists formalized evidence.

Search scope: on 2026-10-07 the site's problem page and thread, the community database (teorth/erdosproblems, data/problems.yaml), the formal-conjectures statement file, the Lean repository named above, the arXiv records and the publisher's record of the journal version were read; no further claim was found. Nothing remains open in the stated question.

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.

Linked from (15)

Lichtman, the primes maximize the Erdős sum over primitive sets Alexeev and coauthors, a shorter proof through von Mangoldt flows problems/divisors/E0164/claims Problem 1196 The von Mangoldt chain bound for primitive sets above x Divisors and Multiples Divisors and Multiples divisors/erdos_1935_note_sequences_integers_no_one_which Theorem (p. 126): for a primitive sequence the sum of 1/(a log a) converges divisors/lichtman_2022_proof_erdos_primitive_set_conjecture Theorem 1.2 (p. 3): f(A) <= f(P) for every primitive set A Theorem 1.3 (p. 3): every odd prime is Erdős strong integer_sequences/alexeev_2026_primitive_sets_von_mangoldt_chains_erdos Theorem 1.2 (p. 3): for every primitive A, f(A) ≤ f(primes) = 1.6366...Theorem 1.4 (p. 4): 2 is Erdős-strong

Graph