E158: “Must every infinite B₂[2] set have liminf-zero square-root-normalized growth?”

Open

Statement	User	Model	Harness	Time
2)V2If S is a finite B₂[2] set contained below N, then the number of unordered pairs from S is at most 4N.	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
1)V1Every infinite set A of natural numbers with at most two unordered representations of each integer as a sum o…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26

2) V2 If S is a finite B₂[2] set contained below N, then the number of unordered pairs from S is at most 4N.

kernel-checked, filed Tue Aug 25 2026 03:50:14 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. All finite S ⊆ ℕ contained in [0,N) and satisfying the exact B₂[2] predicate of the root.

1) V1 Every infinite set A of natural numbers with at most two unordered representations of each integer as a sum of two elements of A satisfies liminf |A∩[0,N)|/sqrt(N) = 0.

open, filed Tue Aug 25 2026 03:49:58 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Search asymmetry: Lean can check a long additive-energy or density-decrement argument while separately certifying every finite representation-count estimate.

Scope. All infinite A ⊆ ℕ satisfying the B₂[2] unordered two-sum representation bound.

E158:Erdős Problem #158 “Must every infinite B₂[2] set have liminf-zero square-root-normalized growth?”

E158: “Must every infinite B₂[2] set have liminf-zero square-root-normalized growth?”