Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Problem 337
claims/: The 2 claim pages of Problem 337, one per claimant's result; the problem's standing derives from them.
Statement. Let be an additive basis (of any finite order) such that . Is it true that
Status. Disproved, the site's label (DISPROVED (LEAN),): Turjányi [Tu84] gave a counterexample basis of every order , Ruzsa and Turjányi [RT85] gave one of every order with the -fold sumset in place of , and their order-3 construction has a Lean 4 proof, the label's Lean qualifier. The accepted claims are Turjányi 1984 and Ruzsa and Turjányi 1985.
Source. erdosproblems.com/337, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #337, https://www.erdosproblems.com/337.
References.
- [RT85] Ruzsa, I. Z. and Turjányi, S., A note on additive bases of integers. Publ. Math. Debrecen (1985), 101-104.
- [Tu84] Turjányi, S., A note on basis sequences. Topics in classical number theory, Vol. I, II (Budapest, 1981) (1984), 1571-1576.
Formalization. Statement in formal-conjectures.
Current assessment
Disproved by Turjányi's 1984 construction (proceedings) and by Ruzsa and Turjányi's refereed 1985 paper. The site's formulation above asks whether every additive basis of finite order with counting function has . The answer is no. Turjányi's 1984 note builds a basis of order with a bounded for every ; Ruzsa and Turjányi's Theorem 1 (1985) builds, for every , a basis of order with and , whose case is a counterexample of order . The repaired forms, both recorded on the second claim page, are their Theorem 2, for every such basis, which the 1985 paper proves, and their Conjecture 1, the same with , which follows from the Plünnecke--Ruzsa inequality applied to , as the formal-conjectures statement file records with that derivation and a formal proof in a contributor's fork. The Lean 4 proof posted to the thread on 2025-12-10 (formal authors Aristotle and Boris Alexeev) formalizes the order-3 construction and gives the site's label its Lean qualifier; the same formal-conjectures file names it as the formal proof of its statement while noting two differences of form, and this project has not built or audited it, so the acceptance rests on the refereed 1985 paper and the site's record. The statements of the 1985 paper are recorded on its source card; no proof is compiled or reviewed here, and Turjányi's note is not held in the library.
Search scope (2026-10-07). The account above rests on the site's problem page and forum thread (one comment, 2025-12-10), the formal-conjectures statement file, the header and theorem statements of the linked Lean file, and the Ruzsa and Turjányi source card. Neither paper's proof is checked here, the Lean file is not built here, and no literature search beyond these sources is recorded.
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.