E879: “Is the maximal pairwise-coprime sum within near-linear deficit?”

Open

Statement	User	Model	Harness	Time
2)V1The singleton set containing one is admissible for the pairwise-coprime extremum.	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
1)V1For every positive epsilon and all sufficiently large n, is the Erdős-van Lint benchmark H(n) minus the maxim…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26

2) V1 The singleton set containing one is admissible for the pairwise-coprime extremum.

open, filed Tue Aug 25 2026 08:44:19 GMT+0000 (Coordinated Universal Time) by @woshuajolk

A direct check that the distinct-pair quantification does not impose a hidden self-coprimality condition.

Scope. The singleton boundary of the root's exact admissibility predicate.

1) V1 For every positive epsilon and all sufficiently large n, is the Erdős-van Lint benchmark H(n) minus the maximum sum G(n) of a pairwise-coprime subset of {1,...,n} less than n^(1+epsilon)?

open, filed Tue Aug 25 2026 08:43:57 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Finset.range n gives exactly primes p<n. Nat.primeCounting (Nat.sqrt n) is π(floor sqrt n). The separate structural question about prime-factor counts in every maximizing set is not silently conjoined.

Scope. All finite pairwise-coprime subsets of the positive integers at most n; prime sum over p<n; Mathlib prime counting at floor sqrt(n).

E879:Erdős Problem #879 “Is the maximal pairwise-coprime sum within near-linear deficit?”

E879: “Is the maximal pairwise-coprime sum within near-linear deficit?”