---

Claim. Let $t(N)$ be the largest number of subsets of $\{1,\ldots,N\}$ whose pairwise intersections are all nonempty arithmetic progressions, the quantity Problem 272 asks for. The Lean proof establishes

$$t(N)=\frac{N^2}{2}+O(N),$$

through the bounds $\binom N2+1\le t(N)\le\binom N2+22051N$ for all large $N$. This answers yes Szabó's linear-error question, the second of the two questions in Section 6 of Szabó's 1999 paper (Szabó's claim page), whether $t(N)=\binom N2+O(N)$, and sharpens Szabó's error term $O(N^{5/3}(\log N)^3)$ to a linear one. The formal statement proved is the catalog variant Erdos272.erdos_272.variants.szabo_strong of the formal-conjectures file for the problem, at the catalog commit the bounty task pinned: with IsArithInterSet N A requiring $A\subseteq\mathcal P(\{1,\ldots,N\})$ and every pair of distinct members to intersect in a progression of some length $l>0$ (one- and two-element sets counted as progressions, as the site's own $\binom N2+1$ example presumes) and maxArithInterCard N the attained supremum of $|A|$, the statement is that $t(N)-N^2/2=O(N)$ with real subtraction and a two-sided big-O. The file's route: the lower bound from $\{1\}$ and all two- and three-element sets containing $1$; for the upper bound, any admissible family with at least $N^2/2$ members reduces, losing at most $2048N$ members, to a family with a common point, which has at most $\binom N2+20001N$ members, or to a family with a long common interval core, which has at most $\binom N2+20003N$, both by private-witness and progression-matching counts. The solver is shown by Conjectures.io as JenW1N; the 12,791-line file declares no author and no AI system, and the library card jenw1n_2026_erdos_problem_272_szabo_strong records Conjectures.io's record, the verified statement, the acceptance timeline and the file's provenance.

Covers. The linear-error asymptotic $t(N)=N^2/2+O(N)$ alone. The exact value of $t(N)$ for general $N$, which the catalog question asks for and which is reported only for $3\le N\le12$ (by computations posted on the site's discussion thread in August 2025 for $N\le9$, and by Yang's unrefereed preprint, which adds $N=10,11,12$; see Yang's claim page), and Szabó's kernel conjecture, that every extremal family has a common element, are not addressed; the bounty site's review note says as much. The problem stays open on the catalog's question.

Depends on. No page of this wiki: the proof is self-contained in its Lean file and uses none of the earlier bounds.

Acceptance. Reviewed: the bounty site Conjectures.io verified the file with its Lean kernel on 9 September 2026 (its report records a static scan with no imports, axiom declarations, sorry, native_decide or unsafe options, the statement unchanged, the axioms propext, Quot.sound and Classical.choice only, and a fresh isolated replay on 10 September 2026), approved it in review on 11 September 2026 under its policy v2, certified the record on 14 September 2026 and paid the bounty. Its review note states that the approval concerns the unrestricted linear-error asymptotic and asserts neither an exact extremal formula nor the kernel conjecture, and calls itself an eligibility decision rather than a guarantee of originality. That certification is documented independent acceptance of the variant. Not formalized in this corpus's sense: this corpus has not built or audited the file, the kernel check is the bounty site's on a single kernel (its second kernel was not run), and no statement-fidelity review of it is recorded; the agreement of the proved type with the catalog's statement rests on Conjectures.io's source-type hash check; the pinned catalog commit was unreachable on 2026-09-27, and the catalog's default branch states the variant identically. Not refereed: there is no write-up and no journal publication; erdosproblems.com labels the problem OPEN with no proof claim on its tab, and the catalog's default branch labels the variant research open, both.