---

Claim. Let $d_k(p)$ be the density of the integers whose $k$th smallest distinct prime factor is $p$. Theorem 5 of Cambie's paper: indexed by the primes in increasing order, $d_k(p)$ is unimodal for $k=1,2,3$ and is not unimodal for every $4\le k\le20$. The question of Problem 690, whether $d_k(p)$ is unimodal for fixed $k\ge1$, is therefore answered no: the failure Erdős expected occurs for every $k$ from $4$ to $20$. The proof writes $d_k(p_i)$ as $\delta_{k-1}(i-1)/p_i$, with $\delta_r(i)$ the density of integers divisible by exactly $r$ of the first $i+1$ primes $p_0=2,\ldots,p_i$, proves the three unimodal cases from the monotone tails of $\delta_0,\delta_1,\delta_2$ and a finite check, and refutes unimodality for $4\le k\le20$ by a computer check of that range (the notebook linked above), printing the $k=4$ and $k=5$ sequences in its appendix, which show the strict valleys $d_4(13)>d_4(17)<d_4(19)$ and $d_5(23)>d_5(29)<d_5(31)$; the library's Theorem 5 page recomputes a strict valley $d_k(a)>d_k(b)<d_k(c)$ for every $k$ in the range with exact rational arithmetic.

Reading of the question. The thread records two readings: is the sequence unimodal for every $k$ (answered no by this theorem), or, for each $k$, decide whether it is (decided by this theorem for $k\le20$ only). On 2026-05-07 the site's curator adopted the first reading and said they would mark the problem solved by the small $k$ counterexamples unless someone defended the wider version; the site marked it solved on 10 May 2026. Under the second reading the remaining $k>20$ are the subject of the pending Wang–Crapis claim. The claim value follows the question's polarity: a yes-or-no question answered no is disproved; the site's label, Solved, stays in the problem page's Status sentence.

Depends on. Nothing in this wiki.

The corpus's transcription of the proof is the library's Theorem 5 page, which recomputed the finite checks with exact rational arithmetic and notes that a printed implication in the source's proof is false in general and is avoided by comparing the $d_k(p)$ values themselves; that transcription is compilation, not acceptance evidence.

Acceptance. Refereed: Journal of Number Theory 280 (2026), 271--277, the peer-reviewed version of arXiv:2501.10333 (v1, 17 January 2025). Reviewed: the site's remarks cite the paper and thank the author, the site labels the problem SOLVED, and the thread post of 2026-05-07 by the site's curator, Thomas Bloom, records the decision to mark it solved by these counterexamples; Bloom is independent of the author.

Lean. Not formalized evidence: this corpus has not built or audited the files linked above, so they give no formalized evidence. The file src/latest/ErdosProblems/Erdos690.lean in Boris Alexeev's lean-proofs repository (GitHub plby), at the pinned revision linked above, declares itself "a Lean formalization of a solution to Erdős Problem 690" with Stijn Cambie as its informal author and Codex and GPT-5.6 Sol as its formal authors, under a copyright line of Joseph Tooby-Smith naming OpenAI Codex as author and a notice that the file was modified; its docstring says it proves the exact natural-density formula for the event that $p$ is the $k$th distinct prime factor and formalizes Cambie's resolution, and its theorem erdos_690 states that conjunction: every $d_k(p)$ exists with the exact rational value, unimodal for $k=1,2,3$, not unimodal for $4\le k\le20$. The file has no sorry and no axiom, imports modules of the Problem 697 formalization, and ends with a #print axioms line without recorded output. As a formalization of the named claimant's result it is a link on this page, not a claim of its own. The formal-conjectures statement erdos_690 and its three solved variants point at its erdos_690 theorem through formal_proof attributes; the statement file is not a formalization link.