---

Claim. For $k\ge2$ let $F_k^{\mathrm{rep}}(n)$ be the largest size of a set $A\subseteq\{1,\ldots,n\}$ in which no member $a$ divides a product $b_1\cdots b_k$ of members of $A\setminus\{a\}$, repetitions allowed, and $F_k^{\mathrm{dist}}(n)$ the same with the $b_i$ distinct; let $S=n^{2/(k+1)}/(\log n)^2$. The theorem main of the Lean file states that for every $k\ge2$ and $\varepsilon>0$, for all large $n$,

$$\pi(n)+(\Lambda_{k+1}-\varepsilon)S\le F_k^{\mathrm{rep}}(n)\le F_k^{\mathrm{dist}}(n)\le\pi(n)+(\Lambda_{k+1}+\varepsilon)S,$$

where $\Lambda_r$ is a dyadic packing constant defined as a supremum, and the theorem Lambda_limit states $\Lambda_r\to e^2$. The case $k=2$ of $F_k^{\mathrm{rep}}$ is the $F(n)$ of Problem 793, whose condition allows $b=c$, so $F(n)=\pi(n)+(\Lambda_3+o(1))n^{2/3}/(\log n)^2$: the constant $C$ exists, and it is the same for the convention requiring $b\ne c$. The file does not evaluate $\Lambda_3$; Chojecki's theorem gives the value $27/2$ (its claim page). The file also states two self-contained corollaries for large $k$, with constants $e^2\pm\varepsilon$.

Submission note. Posted to erdosproblems.com as a proof claim by Wouter van Doorn (account Woett) on 5 August 2026, giving "GPT-5.5 Pro and Aristotle" as the AI used:

Let $F_k(n)$ denote the cardinality of the largest set $A \subseteq {1, 2, \ldots, n}$ such that $a \mid b_1b_2 \cdots b_k$ with $a, b_1, \ldots, b_k \in A$ implies $a \in \{b_1, b_2, \ldots, b_k\}$. Then Erdős conjectured the existence of a constant $c_k$ such that

$$> F_k(n) = \pi(n) + \frac{(c_k + o(1))n^{2/(k+1)}}{\log^2 n}. >$$

The case $k = 2$ is the original problem and was solved (with constant $c_2 = 27/2$) here and formalized here. This proof claim is mainly to record that the generalization is now also formalized with a constant $c_k$ that converges to $e^2$ as $k$ goes to infinity. Notes: I feel a bit guilty sharing this, as I have not digested the proof myself and don't expect to in the near future. But I hope it's sufficiently interesting anyway.

Claimant and postings. The site lists the entry of 5 August 2026 as a proof claimed by Wouter van Doorn (the account Woett) using GPT-5.5 Pro and Aristotle, with no kind. The blueprint's byline is ChatGPT, and it calls itself AI-generated and not independently verified; the Lean file's header says that Aristotle, from Harmonic, formalized the result from a ChatGPT write-up. The submitter's note says the submitter has not digested the proof.

Formalization. The file contains no sorry and declares two axioms: pi_alt, the prime number theorem, and DP_empty, the file's own specialization of Theorem 1.11 of M. Delcourt and L. Postle, arXiv:2204.08981, used only in the lower bound. Nothing was built or audited in this corpus, so the page does not list formalized.

Depends on. No page of this wiki.

Standing. Claimed: no refereed publication, independent review or formalization built in this corpus is on record.