Erdős problem 1062 — wave w030
Date: 2026-07-29 UTC
Claim labels
- (a) elementary-rigorous: proved below directly from the definition.
- (b) rigorous-modulo-named-theorem: conditional on the cited theorem or
preprint proof being correct.
- (c) plausible/structural-unverified: an identified direction, not a
theorem.
- (d) computational-only: exact finite solver output, with the stated
independent checks, but without a formally checked UNSAT certificate.
Status observations and bibliographic facts are identified as such rather than assigned mathematical claim labels.
0. Mandatory live-page gate
I fetched both the live problem page and its discussion thread through the Bright Data browser path on 2026-07-29. Direct datacenter access was not used for the gate.
Exact current statement
The following is verbatim from the page's “View the LaTeX source” view:
Let \(f(n)\) be the size of the largest subset \(A\subseteq \{1,\ldots,n\}\) such that there are no three distinct elements \(a,b,c\in A\) such that \(a\mid b\) and \(a\mid c\). How large can \(f(n)\) be? Is \(\lim f(n)/n\) irrational?
Status and no-collision decision
The live page showed:
OPEN;- 0 claimed proofs;
- “Interested in collaborating”:
None; - “Currently working on this problem”:
None; - 13 comments;
- the main page last edited 06 January 2026;
- a formalised statement link and related OEIS sequence A038372.
Thus the explicit claimed-proof and current-worker stop markers were both absent. The discussion does contain a claimed partial result from April 2026, but the site's claimed-proofs counter remains zero, Thomas Bloom calls it partial rather than a full solution, and the author explicitly leaves irrationality open. I therefore passed the gate but did not duplicate the claimed asymptotic work; the contribution below is an exact finite table.
Results listed on the live page
The page gives the interval example \([m+1,3m+2]\), yielding
and reports that Lebensold [Le76] proved, for large \(n\),
It identifies this as Problem B24 in Guy's collection [Gu04].
All 13 comments, grouped chronologically
The following is a faithful content summary, not an endorsement of the unverified user comments.
- 28 September 2025 (three comments). Thomas Bloom said he could not
access Lebensold's paper, but its MathSciNet review suggested that more computation in Lebensold's method could sharpen the numerical bounds. Vjeko Kovač identified \(n\mapsto f(n)\) as OEIS A038372 and asked for it to be added to the page; Bloom replied that this was done.
- 05 January 2026 (one comment). Yongxi Lin corrected the elementary
bound from a floor to \(f(n)\geq\lceil 2n/3\rceil\), using \(\{\lfloor n/3\rfloor+1,\ldots,n\}\).
- 19–20 April 2026 (three comments). Damek Davis claimed a partial
result: existence of an effectively computable extremal density and counting rate using McNew's divisor-graph theorem, while leaving irrationality open; he linked a paper. Nat Sothanaphan reported that a “standard check” found no issue. Przemek Chojecki linked separate GPT-5.4-generated notes using the same McNew approach.
- 04 May 2026 (six comments). MalekZ asked why the problem remained
open. Bloom replied that he had not reviewed the claimed partial solution and that, even if correct, it does not answer irrationality. MalekZ asked about automatic closure after Lean verification; Bloom explained that nothing is automatic and the formal statement/proof still requires checking. Sothanaphan pointed to the AI wiki's partial-result section, and MalekZ acknowledged the distinction.
The forum itself warns that comments are user-supplied and unverified.
1. Literature audit
I searched the exact title, problem wording, Guy B24, Lebensold's paper, OEIS A038372, and McNew's divisor-graph theorem. The relevant sources found were:
- Guy. The official Springer record verifies Richard K. Guy,
Unsolved Problems in Number Theory, third edition, Springer, 2004, DOI 10.1007/978-0-387-26677-0. The live page identifies the question as B24.
- Lebensold. Kenneth Lebensold, “A Divisibility Problem,” *Studies in
Applied Mathematics* 56 (1977), 291–294, DOI 10.1002/sapm1977563291. The DOI, author, volume, issue, and pages are independently present in bibliographic indexes. Wiley returned a Cloudflare verification page even through the browser path, so I did not inspect the original article text. I therefore use the \(0.6725/0.6736\) attribution only because it is ground truth on the live page and is repeated in the 2026 preprint below; I do not claim a direct audit of Lebensold's proof.
- McNew. Nathan McNew,
“Counting primitive subsets and other statistics of the divisor graph of \(\{1,2,\ldots,n\}\)”, arXiv:1808.04923, published in European Journal of Combinatorics 92 (2021), 103237. The paper's Theorem 3 is the named local-statistics input used by the April 2026 work.
- Chojecki/OpenAI note. The comment-linked nine-page note,
“A note on Erdős problem #1062: Asymptotic density, initial layers, and local structure”, dated 15 April 2026, claims via McNew that the density exists, identifies the first four series layers \(w_1=1/2,w_2=1/6,w_3=0,w_4=1/270\), and observes that the fifth layer already has infinitely many rooted component types. This is a comment-linked AI-generated note, not a result I treat as independently certified here.
- Davis preprint. The comment's “arXiv TBA” paper now exists as Damek
Davis, “Forbidden subgraphs in divisor graphs and an Erdős divisibility problem”, arXiv:2604.17613v1, submitted 19 April 2026. (b) Conditional on its proof of the McNew specialization, it proves \[ f(n)=c_2n+ O_\varepsilon\!\left( n\exp\bigl(-(1-\varepsilon)\sqrt{\log n\log\log n}\bigr) \right) \] for an effectively computable \(c_2\), so the limit exists. It explicitly says irrationality remains open. (d, as reported by that preprint) Its CP-SAT truncation gives \(c_2\geq0.6729\), while it retains Lebensold's \(c_2\leq0.6736\).
- Small exact values. OEIS A038372 contained
only \(f(1),\ldots,f(44)\) on the access date. Its entries agree exactly with the first 44 values recomputed below. Neither the Davis preprint nor the Chojecki/OpenAI note lists global values such as \(f(100)\).
Exact-phrase and citation searches found no primary source claiming irrationality or giving a longer exact global table. This is a search miss, not a proof that no such source exists.
2. New finite result
Exact table through 200
(d) Computational-only exact result. For every \(1\leq n\leq200\),
where
Thus the elementary interval construction is exactly optimal on the five \(\delta_n=0\) ranges, and the first verified improvement by two elements is the whole interval \(189\leq n\leq200\).
OEIS already contained \(n\leq44\). The newly computed extension is:
| \(n\) | \(f(n)\), in increasing order of \(n\) | |---:|:---| | 45–60 | 30, 31, 32, 32, 33, 34, 34, 35, 36, 37, 38, 39, 39, 40, 41, 41 | | 61–80 | 42, 43, 43, 43, 44, 44, 45, 46, 46, 47, 48, 48, 49, 50, 50, 51, 52, 52, 53, 54 | | 81–100 | 55, 56, 57, 57, 58, 59, 59, 60, 61, 61, 62, 63, 63, 64, 65, 65, 66, 67, 67, 68 | | 101–120 | 69, 69, 70, 71, 71, 72, 73, 73, 74, 75, 75, 76, 77, 77, 78, 79, 79, 80, 81, 81 | | 121–140 | 82, 83, 83, 84, 85, 85, 86, 86, 86, 87, 88, 88, 89, 90, 91, 92, 93, 93, 94, 95 | | 141–160 | 95, 96, 97, 97, 98, 99, 99, 100, 101, 101, 102, 103, 103, 104, 105, 105, 106, 107, 107, 107 | | 161–180 | 108, 109, 110, 111, 111, 112, 113, 113, 114, 115, 115, 116, 117, 117, 118, 119, 119, 120, 121, 121 | | 181–200 | 122, 123, 123, 124, 125, 125, 126, 127, 128, 129, 130, 130, 131, 132, 132, 133, 134, 134, 135, 136 |
Explicit endpoint construction
(a) Lower bound at the endpoint. The following set has 136 elements:
Here \(u\text{--}v\) denotes every integer from \(u\) through \(v\). The standalone checker counts the elements and, for every \(a\in A_{200}\), directly counts the other selected multiples of \(a\); that count never exceeds one. Hence \(f(200)\geq136\) without trusting the optimization encoding.
(d) Upper bound at the endpoint. Both exact MaxSAT runs return optimum cost 64 for \(n=200\), hence \(f(200)\leq200-64=136\). Together with the directly checked construction,
3. Exact finite reduction
For \(1\leq i\leq n\), let \(x_i=1\) mean \(i\in A\).
Soundness and completeness of the clauses
(a) Fix \(a\), and let \(b<c\) be two distinct proper multiples of \(a\) not exceeding \(n\). The original condition forbids selecting all three, which is exactly the Boolean clause
Conversely, any forbidden triple in the statement has a divisor \(a\) and two distinct other selected multiples \(b,c\). Positive proper multiples are larger than \(a\), so after exchanging \(b,c\) if necessary it occurs exactly once in the generated list
Thus satisfying every clause (1) is equivalent, not merely necessary, to the problem's condition.
Add a soft unit clause \(x_i\) of weight one for every \(i\). For any model of the hard clauses, the number of false soft clauses is exactly \(n-\sum_i x_i=n-|A|\). Therefore
Equation (2) is an elementary exact reduction. The assertion that a particular solver found OptCost is claim (d).
The core model-building code is:
def forbidden_triples(n):
for a in range(1, n // 3 + 1):
multiples = range(2 * a, n + 1, a)
for b, c in itertools.combinations(multiples, 2):
yield a, b, c
formula = WCNF()
for a, b, c in forbidden_triples(n):
formula.append([-a, -b, -c]) # hard
for i in range(1, n + 1):
formula.append([i], weight=1) # soft
with RC2(formula, solver=solver_name,
adapt=True, exhaust=True, incr=True) as optimizer:
model = optimizer.compute()
value = n - optimizer.cost
At \(n=44,100,200\), the independently regenerated hard-clause counts are respectively \(1300,7435,31048\).
4. Reproduction and independent checks
The standalone re-verifier is erdos1062_wavew030_reverify.py. Its SHA-256 is
81fefb0ccf216abca49c0e9d8dc0a12c3d8448f56f4df6f91b3399b6d134f073
Run it from the repository root with:
python3 runs/erdos1062_wavew030_reverify.py
It performs four checks:
- (a) Directly enumerates every subset, without SAT, for
\(1\leq n\leq18\).
- (d) Rebuilds and solves all 200 WCNFs twice, using the separately
compiled PySAT Glucose 3 and Glucose 4 engines. The returned tables agree entry by entry.
- (a) Checks every returned witness, and the saved \(A_{200}\), directly
against divisibility rather than against clauses.
- (d) If CBC is installed, independently rebuilds the binary ILP
\[
\max\sum_i x_i,\qquad x_a+x_b+x_c\leq2
\] and requires CBC to report Optimal for the spot check \(f(100)=68\).
The exact saved run was:
direct enumeration n=1..18 agrees
Glucose3/RC2 complete: f(200)=136
Glucose4/RC2 complete: f(200)=136
delta=0 ranges: 1-26, 32-53, 64-80, 128-134, 160-161
delta=1 ranges: 27-31, 54-63, 81-127, 135-159, 162-188
delta=2 ranges: 189-200
CBC independent binary-ILP spot check complete: f(100)=68, witness_size=68
PySAT 1.9.dev7
hard clauses: {44: 1300, 100: 7435, 200: 31048}
elapsed_seconds=16.272
VERIFIED: exact computational table f(1)..f(200);
new range beyond OEIS is n=45..200; f(200)=136
TIME_ELAPSED=16.34 MAXRSS_KB=69660
The first 44 recomputed values agree with every entry then present in OEIS A038372. This catches a historical-data mismatch but is not used as an optimality oracle.
5. What remains and the precise irrationality wall
This finite computation does not resolve the asymptotic irrationality question.
(b) Accepting the McNew-based April 2026 arguments, the constant has an explicit, effectively convergent series whose terms are determined by finite rooted divisor-component optimizations. Effective computability and arbitrarily tight rational intervals do not imply irrationality: rational numbers are dense, and there is no known denominator bound for a hypothetical rational value of \(c_2\).
The exact missing ingredient is therefore not more values of \(f(n)\), but one of the following uniform statements:
- an identity reducing the infinite McNew series to a closed expression
with a provably irrational component and controlled cancellation; or
- an arithmetic non-cancellation theorem proving that the complete weighted
sum cannot be rational.
(c) The finite-layer route currently stalls at precisely this point. The linked Chojecki/OpenAI note's infinite family of fifth-layer rooted component types explains why a finite-state or eventually periodic tail cannot simply be assumed. A finite truncation plus a numerical tail bound can improve decimals, but without a denominator-exclusion lemma it cannot separate \(c_2\) from every rational number. The exact table through 200 supplies local evidence and reusable test cases, not that missing uniformity theorem.
PARTIAL: Exact computational values f(n) are independently reproduced through n=200 (extending OEIS n=45..200), with f(200)=136 and an explicit checked witness; irrationality remains open and requires a uniform arithmetic non-cancellation theorem for the infinite McNew series.