---

Claim. Call a set of positive integers free of forbidden triples when it has no $a,b,c$ with $a<\min(b,c)$ and $a\mid b+c$, with $b=c$ allowed, which is the site's reading of the condition and Bedert's Definition 1. Bedert proves that there is an absolute constant $C$ such that every such $A\subseteq\{1,\ldots,N\}$ has $|A|\le N/3+C$ (Theorem 1), and that for all sufficiently large $N$ such a set has $|A|\le\lceil N/3\rceil$, which the set $\{\lfloor2N/3\rfloor+1,\ldots,N\}$ attains (Theorem 2). Theorem 1 answers the problem's question yes; Theorem 2 gives the exact maximum for large $N$. The source is B. Bedert, On a problem of Erdős and Sárközy about sequences with no term dividing the sum of two larger terms, arXiv:2301.07065v1 (17 January 2023), 43 pp., with the library pages Theorem 1 and Theorem 2 on the source card.

Acceptance. The claim is accepted on the review of Thomas Bloom, the site's curator, who is independent of the claimant: the problem page, labeled PROVED (LEAN) and last edited 8 April 2026, names Bedert's paper in its commentary as the proof that the answer is yes (accessed 2026-09-18); its discussion thread and proof-claim tab were empty. The formal-conjectures collection marks its statement of the problem research solved. No journal version was found on 2026-09-18 (the arXiv record lists none, a Crossref bibliographic query returned no record, and zbMATH Open lists the preprint only), no citing paper was found through Semantic Scholar, and no dispute was found. The proof (pp. 3--43) was not read in this repository, and this page rests on no review of its own.

Formalization. One Lean file is linked: Erdos13.lean of Boris Alexeev's collection lean-proofs at the pinned commit, which describes itself as a Lean formalization of a solution to the problem, names Bedert as the informal author and Codex and GPT-5.6 Sol as the formal authors, and proves the $N/3+C$ statement from an internal bound, with no sorry, axiom declaration or native_decide in its text. It was not built or audited here, so it is linked and not counted as formalized. The formal-conjectures file that states the theorem with a sorry body is described on the problem page; a statement file is not a formalization and is not linked here. The site's (LEAN) suffix is its catalog label; the community database lists formal_status as Lean, as of a last update dated 23 August 2026, and has no field for a formal proof's location. On 18 September 2026 formal-conjectures registered the linked Erdos13.lean as the formal_proof of its statement of the problem.

Scope. Full for the site's statement. Erdős's own finite conjecture, which forbids a term dividing the sum of two distinct larger terms and puts the maximum at $[x/3]+1$, is a variant that the theorems as stated do not decide, and the $r$-fold generalization is open; the problem page describes both.

Depends on. Theorem 1 of Bedert 2023 and Theorem 2, the result pages of the cited preprint.