Problem 862

../

claims/: The 1 claim page of Problem 862, one per claimant's result; the problem's standing derives from them.

---

Statement. Let $A_1(N)$ be the number of maximal Sidon subsets of $\{1,\ldots,N\}$. Is it true that

$$A_1(N) < 2^{o(N^{1/2})}?$$

Is it true that

$$A_1(N) > 2^{N^c}$$

for some constant $c>0$?

Status. Solved. The site labels the problem SOLVED (LEAN) and records both questions as answered by Saxton and Thomason's count of Sidon sets, the first no and the second yes, and its label carries a Lean qualifier for an automatically produced Lean proof whose first posting assumed a prime-gap axiom that a later revision removes; the accepted claim is Saxton and Thomason.

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

References.

• [SaTh15] Saxton, David and Thomason, Andrew, Hypergraph containers. Invent. Math. 201 (2015), 925-992.
• [SaTh16] Saxton, David and Thomason, Andrew, Online containers for hypergraphs, with applications to linear equations. J. Combin. Theory Ser. B 121 (2016), 248-283; arXiv:1611.01433. Theorem 1.10 and Section 5 give the proof of the Sidon-set count stated as Theorem 2.11 of [SaTh15].

Formalization. Statement in formal-conjectures. A Lean 4 proof of the conclusion, posted on 2026-01-21 in lean-proofs, was produced automatically by Aristotle (from Harmonic) from a proof of ChatGPT's choice, with the theorem statement written by Aristotle; its first posting assumed one axiom beyond Lean's standard three, a prime between $x$ and $(1+\varepsilon)x$ for all large $x$, which a later revision of 2026-06-24 or earlier removes; this corpus has audited neither. Details on the claim page.

Progress

Not yet compiled.

Known Results

Not yet compiled.

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.

• saxton_2015_hypergraph_containers
• saxton_2015_hypergraph_containers / theorem_2_11