ERDŐS/DAILY ▸

← back to the ledger

ERDőS #425 · PARTIAL

Erdős problem #425 — wave 9i

Date of audit: 2026-07-28 UTC.

Claim labels

No claim about solving either asymptotic question is made.

0. Mandatory live-page check

(a, direct observation) I fetched the live page through the Bright Data browser route, not datacenter curl. On 2026-07-28 the page Erdős Problems #425 displayed:

Thus neither mandatory stop condition was present.

Verbatim live statement

The following is copied verbatim from the page's LaTeX-source view, including the capital \(N\) in the first displayed universe:

Let $F(n)$ be the maximum possible size of a subset $A\subseteq\{1,\ldots,N\}$ such that the products $ab$ are distinct for all $a<b$. Is there a constant $c$ such that\[F(n)=\pi(n)+(c+o(1))n^{3/4}(\log n)^{-3/2}?\]If $A\subseteq \{1,\ldots,n\}$ is such that all products $a_1\cdots a_r$ are distinct for $a_1<\cdots <a_r$ then is it true that\[\lvert A\rvert \leq \pi(n)+O(n^{\frac{r+1}{2r}})?\]

(a) The occurrence of \(N\) makes the first sentence literally ill-typed as a definition of \(F(n)\). The formula that follows, the second question, and all page remarks use \(n\). The finite computation below makes the explicit interpretation \(N=n\); it does not silently alter the quoted statement.

Results and remarks listed on the live page

(b, Erdős 1938/1969) The page states that there are constants \(0<c_1\leq c_2\) for which

\[ \pi(n)+c_1\frac{n^{3/4}}{(\log n)^{3/2}} \leq F(n)\leq \pi(n)+c_2\frac{n^{3/4}}{(\log n)^{3/2}}. \]

It attributes the lower bound to Erdős's 1938 paper and the matching-order upper bound to Erdős's 1968/69 paper.

(b, cited page sources) The page also records the real variant asking for the largest \(A\subset[1,x]\) with \(\lvert ab-cd\rvert\geq1\) for distinct \(a,b,c,d\in A\). It says that Erdős's conjecture \(\lvert A\rvert=o(x)\) was disproved by Alexander. The displayed construction starts with an integer Sidon set \(B\subset[1,X^2]\), \(|B|\gg X\), and takes

\[ A=\{Xe^{b/X^2}:b\in B\}. \]

After constant rescaling it has \(\gg X\) elements in \([X,O(X)]\), with a modification making it 1-separated. The page also mentions a complex-number generalisation and points to problems 490, 793, and 796.

All seven live comments

The site explicitly warns that comments are not verified. Accordingly, every item in this subsection is labelled (c) unless a narrower numerical check is stated.

  1. (c) Woett, 5 May 2026: a Lean/PNT lower-bound project claiming every

coefficient \(c<2^{11/4}/3^{3/4}\approx2.95115\); the proposed upper-bound formalisation was then unfinished.

  1. (c) vilc, 5 May 2026: a projective-plane sketch giving

\(c=2^{3/4}\approx1.68179\).

  1. (c) Woett, 5 May 2026: link to the generated lower-bound blueprint.
  2. (c) vilc, 6 May 2026: a 20-layer optimisation report suggesting

\(2^{11/4}/3^{3/4}\) is optimal inside that layered construction.

  1. (c) Woett, 17 May 2026: an upper-bound formalisation claiming

\(c> C_*<13.1\), conditional on named Dusart, Buchstab, and integral inputs and using native_decide.

  1. (c) KentaKitamura, 6 June 2026: a natural-language Bellman-inequality

argument claiming \(2^{11/4}/3^{3/4}\) is the exact supremum only within the rectangular layered semiprime ansatz, explicitly not a global upper bound.

  1. (c) KentaKitamura, 6 June 2026, edited 11 June: an “attempt report”

and Lean repository claiming, from PNT, every lower coefficient \(c<3.499\). This is a partial lower bound, not a claim that #425 is solved; the live page still lists zero claimed proofs.

(d, numerical subclaim only) I cloned the repository in comment 7 at commit 9366b2bd2830d4073551a44217ca5ba1b0953a30. Its stated theorem erdosF_lower_3499_PNT exists. Running

python -X int_max_str_digits=0 exp/01_interval_c12.py
python -X int_max_str_digits=0 exp/06_extended_certificate.py

reproduced \(C_{12}>3.499\) and

\[ C_{20}\in[3.499012635397,3.499012635397]. \]

This checks the repository's coefficient arithmetic only. I did not spend the much larger dependency/build budget needed to kernel-check its full 5,400-line Lean development, so its structural and asymptotic theorem remains labelled (c) in this report.

1. Focused primary-source literature audit

(b) The following named sources were opened and checked, rather than inferred from titles:

On sequences of integers no one of which divides the product of two others and on some related problems (1938). Section 2 defines the pair-product problem, proves \(\pi(n)+O(n^{3/4})\) as an upper bound, and gives the \(n^{3/4}(\log n)^{-3/2}\)-scale lower construction.

Some applications of graph theory to number theory (1969). Equation (4), pp. 78–79, gives matching-order upper and lower bounds and identifies the \(C_4\)-free graph mechanism.

The number of multiplicative Sidon sets of integers, arXiv:1808.06182. Its introduction still records the extremal size only as \(\pi(n)+\Theta(n^{3/4}(\log n)^{-3/2})\); its new theorem is enumerative.

Finding large additive and multiplicative Sidon sets in sets of integers, published online in 2024 and in Mathematische Annalen in 2025. Its introduction likewise cites the same two-sided \(\Theta\)-scale estimate, not a limiting coefficient.

Generalized multiplicative Sidon sets, and An improved upper bound for the size of the multiplicative 3-Sidon sets, arXiv:1801.08733. These forbid an equality between two products of \(k\) pairwise distinct, disjoint elements. For \(k=3\), the latter proves an upper bound with main term \(\pi(n)+\pi(n/2)\); this is weaker than and not identical to the injectivity of all 3-subset products asked on #425.

Recovering affine-linearity of functions from their restrictions to affine lines, explicitly uses “weak multiplicative \(B_h\)-set” for injectivity of the product map on \(h\)-element subsets. Its application concerns rings and affine-linearity, not the extremal interval bound in #425.

(c, search diagnosis) Exact-phrase, arXiv, DOI, citation, and exact-small- value searches found no primary source resolving the limiting constant, the higher-\(r\) bound, or tabulating the strict-pair \(F(n)\) values below. This is a report of the searches performed, not a proof that no such source exists. The authoritative live page remains open and records only partial comment activity.

2. Elementary finite reduction

Fix \(n\), and interpret the first statement with universe \([n]\).

Lemma 1 (a). If \(\{a,b\}\ne\{c,d\}\) are strict pairs of positive integers and \(ab=cd\), then \(a,b,c,d\) are pairwise distinct.

Proof. If the two pairs share an endpoint, cancel that positive endpoint; the other endpoints are equal, so the pairs were the same. \(\square\)

Define the 4-uniform hypergraph \(H_n\) on \([n]\) by

\[ E(H_n)= \bigl\{\{a,b,c,d\}:a<b,\ c<d,\ \{a,b\}\ne\{c,d\},\ ab=cd\bigr\}. \]

Lemma 2 (a). A set \(A\subseteq[n]\) satisfies the page's strict-pair condition if and only if it contains no edge of \(H_n\). Consequently,

\[ F(n)=\alpha(H_n)=n-\tau(H_n), \]

where \(\tau\) is the minimum vertex-cover number.

Proof. Lemma 1 makes every repeated product exactly a four-vertex hyperedge. Avoiding all such edges is precisely independence. Complements exchange independent sets and vertex covers. \(\square\)

There is also the standard rectangle parameterisation. If \(ab=cd\), put \(g=\gcd(a,c)\), \(a=gx\), \(c=gy\), and \(\gcd(x,y)=1\). Then \(xb=yd\), so \(b=hy\), \(d=hx\) for an integer \(h\). Thus every edge is a nondegenerate multiplicative rectangle

\[ \{gx,gy,hx,hy\}. \]

This paragraph is (a) and is explanatory; the checker does not rely on the parameterisation.

3. Exact computation

Result

(d) Exhaustive search gives the complete strict-pair table through 50:

n :  1  2  3  4  5  6  7  8  9 10
F :  1  2  3  4  5  5  6  6  7  7

n : 11 12 13 14 15 16 17 18 19 20
F :  8  9 10 10 10 11 12 12 13 13

n : 21 22 23 24 25 26 27 28 29 30
F : 13 14 15 15 16 16 16 16 17 17

n : 31 32 33 34 35 36 37 38 39 40
F : 18 19 19 19 20 20 21 21 21 21

n : 41 42 43 44 45 46 47 48 49 50
F : 22 23 24 24 24 24 25 25 26 26

A terminal lower-bound witness, already contained in \([49]\), is

\[ \begin{split} A_{50}=\{& 1,3,7,11,16,17,19,23,25,26,27,29,31,34,35,36,37,39,\\ &40,41,42,43,44,45,47,49\}. \end{split} \]

The checker directly forms all \(\binom{26}{2}=325\) strict-pair products and verifies that they are distinct.

Why the upper bounds are exhaustive

(a, correctness of the algorithm; d, its finite output) For a proposed upper bound, the checker asks whether \(H_n\) has a cover of a given budget. At a search state it keeps:

If an uncovered edge has one available vertex, that vertex is forced. If an edge has candidates \(v_1,\ldots,v_t\), the search branches on the first candidate used by a putative cover: branch \(i\) selects \(v_i\) and excludes \(v_1,\ldots,v_{i-1}\). These branches are disjoint and cover every possible completion. Two lower bounds are safe:

  1. uncovered-edge count divided by maximum current vertex degree;
  2. a greedily found collection of edges with pairwise disjoint candidate

sets.

Memoisation only identifies equal pairs (uncovered_edges, available_vertices). Every recursive choice hits the selected edge, so the uncovered-edge bitset strictly decreases and no provisional memo entry can be used cyclically.

The checker exploits monotonicity without omitting a case. For each constant table plateau \([\ell,h]\) of value \(k\):

  1. it constructs and directly product-checks a size-\(k\) witness in

\([\ell]\), proving \(F(n)\geq k\) for every \(n\geq\ell\);

  1. it exhaustively proves that \(H_h\) has no cover of size \(h-k-1\), hence

\(\tau(H_h)\geq h-k\) and \(F(h)\leq k\);

  1. monotonicity gives \(F(n)\leq F(h)\leq k\) for \(n\leq h\).

Together these prove every displayed finite value, conditional only on the execution of the supplied finite integer program.

Independent checks and audit transcript

(d) The verifier performs three deliberately different checks.

  1. It generates collisions by grouping all pairs according to their product.
  2. Independently, it inspects all \(\binom{50}{4}\) four-subsets and their

three pairings. The two generators agree on exactly 728 hyperedges.

  1. Independently of both the hypergraph and cover search, it enumerates

ordinary combinations to reprove \(F(20)=13\) from direct pair products.

On Python 3.12.3, the final audit printed:

independent edge generators agree: |E(H_50)|=728
independent direct-combination check: F(20)=13,
  witness=(1, 2, 4, 6, 7, 9, 11, 13, 15, 16, 17, 19, 20)
...
F(n)=26 for 49<=n<=50:
  upper search@50 budget=23, nodes=120900, time=10.429s
total recursive nodes (all searches): 324826
wall time: 26.754s
VERIFIED

Wall time is machine-dependent; the node counts are deterministic.

4. Reproduction code

The full standard-library-only source is runs/erdos425_wave9i_verify.py. It is the code used to produce the table, not a post-hoc witness-only validator.

Run from the repository root:

python runs/erdos425_wave9i_verify.py

The audited file has 391 lines and SHA-256

a61198b50ed274ca06969b22ea7ba4d5522b74f9388130e28046b93af7d0f322

Its proof-critical recursion is, in pseudocode matching the source:

cover(uncovered, available, budget):
    force every vertex that is the sole available candidate of an edge
    reject if an edge has no candidate or forced vertices exceed budget
    accept if no edge remains
    reject if either safe cover lower bound exceeds budget
    choose an uncovered edge with candidates v1,...,vt
    for i=1,...,t:
        choose vi
        exclude v1,...,v(i-1)
        recurse after deleting every edge hit by vi
    reject

The adjacent .py contains the exact integer bitset implementation, both independent edge generators, the direct product checker, the expected table, all assertions, and the full output routine.

5. A clean reduction for the higher-\(r\) question

Lemma 3 (a). Suppose the product map on the \(r\)-element subsets of \(A\) is injective and \(|A|\geq2r\). For every \(1\leq k\leq r\), there cannot be disjoint \(k\)-element subsets \(X,Y\subset A\) with \(\prod X=\prod Y\).

Proof. If such \(X,Y\) existed, choose an \((r-k)\)-subset \(T\subset A\setminus(X\cup Y)\). This is possible because

\[ |A\setminus(X\cup Y)|\geq2r-2k\geq r-k \]

when \(k\leq r\). (More sharply, \(|A|\geq r+k\) suffices for this fixed \(k\).) The distinct \(r\)-subsets \(X\cup T\) and \(Y\cup T\) then have equal products, a contradiction. \(\square\)

Thus #425's condition implies all of the usual “disjoint multiplicative \(k\)-Sidon” conditions up to \(r\), but the converse fails: the #425 condition also controls equal products of overlapping \(r\)-subsets after cancellation.

For \(r=3\), the \(k=2\) consequence alone gives only the classical \(\pi(n)+O(n^{3/4}(\log n)^{-3/2})\) bound. Pach's disjoint \(k=3\) theorem has the larger main term \(\pi(n)+\pi(n/2)\). Neither separately implies the desired \(\pi(n)+O(n^{2/3})\). This identifies the missing ingredient: one needs an extremal argument exploiting the simultaneous 2-product and 3-product restrictions, not another application of either known theorem in isolation.

6. What remains and the precise wall

(a) Define the normalised correction

\[ D(n)=\frac{(F(n)-\pi(n))(\log n)^{3/2}}{n^{3/4}}. \]

The first question asks whether \(D(n)\) converges. A finite table, however long, cannot supply the uniform \(n\to\infty\) step.

(c, structural diagnosis) The classical factorisation argument maps selected integers to edges of arithmetic host graphs, and a repeated product creates a \(C_4\). To determine a constant one needs both:

  1. an asymptotically sharp weighted \(C_4\)-free extremal theorem for the

nonuniform factorisation host under \(pq\leq n\), uniformly across all factor-size layers; and

  1. a stability/reduction theorem proving that arbitrary near-extremal

multiplicative Sidon sets lose only \(o(n^{3/4}(\log n)^{-3/2})\) when reduced to the host structures covered by that extremal theorem.

The live comments' \(3.499\) construction, even if its Lean theorem is accepted, addresses the lower half only. The \(13.1\) comment is an axiom-dependent upper estimate, not a matching extremal/stability theorem. Optimising more rectangular layers is explicitly reported to stop near 2.951 and therefore cannot close the gap. The exact missing object is a matching global upper theorem for the enlarged polarity/hyperbola host (or a counterconstruction showing that even that host is not universal).

For the second question, Lemma 3 shows why the existing disjoint multiplicative \(k\)-Sidon results do not finish the job. Already at \(r=3\) the needed new lemma must combine the \(C_4\)-type and \(C_6\)-type obstructions strongly enough to remove the \(\pi(n/2)\) term while improving the residual exponent from \(3/4\) to \(2/3\).

No bounded computation has a finiteness or uniformity mechanism that would turn either missing lemma into a theorem, so launching a larger exact search would not responsibly claim progress on the asymptotic closure. The finite search was therefore stopped at the fully replayable \(n\leq50\) table.

PARTIAL: Exact strict-pair values F(1),...,F(50) are exhaustively verified with a standalone checker; the asymptotic constant and higher-r bound remain open, with the missing uniform extremal/stability lemmas isolated above.

This is the AI working report, labelled by outcome — not an independently verified claim unless marked PROVED. ← ledger