---

Claim. The answer is yes. Vinogradov's three-primes theorem, in the form that every sufficiently large odd integer is a sum of three distinct primes, gives a threshold $N$ such that every prime $p>N$ is a sum of three distinct primes, each smaller than $p$. Take $Q_0$ to be the set of all primes at most $N$. By induction on $p$, every prime lies in some $Q_i$: a prime $p>N$ is $p_1+p_2+p_3$ with distinct $p_j<p$, each in some $Q_{i_j}$, so $p$ lies in $Q_{i+1}$ for $i=\max_j i_j$. The sets $Q_i$ therefore exhaust the primes and their sizes are unbounded. The distinct-primes form of Vinogradov's theorem is a small modification of his proof: the number of representations of a large odd $n$ as a sum of three primes grows like $n^2$ up to logarithmic factors, while the representations with two equal primes number $O(n)$.

Postings. Rudi Mrazović and Vjekoslav Kovač sent the observation to the site before its forum existed; the communication itself is undated, and this page is dated by the earliest dated record of the credit, an archived copy of the site's page of 9 December 2024, which already carries the argument, the label SOLVED (the site's label vocabulary at the time) and thanks to Alon, Mrazović and Kovač; an archived copy of 21 July 2024 shows the problem OPEN without the credit. The community database records the PROVED label from 31 August 2025, the date its history begins. In a thread comment of 1 January 2026 Kovač restates the argument and the distinctness modification. There is no paper.

Acceptance. The site's curator, Thomas Bloom, wrote the argument into the commentary of Problem 471, labeled the problem PROVED and thanks Alon, Mrazović and Kovač on the page; that documented acceptance by a curator who had no part in the result is the reviewed evidence. Alon's independent observation of the same argument is the sibling page Alon. Nothing was reviewed here; the argument is an elementary deduction from a classical theorem.

Formalization. The file Erdos471.lean in Boris Alexeev's repository lean-proofs, linked above at a pinned commit and added on 21 August 2026, declares itself a formalization of a solution to Erdős Problem 471, naming Mrazović (the first name misprinted as Luka), Kovač and Alon as informal authors and Codex and GPT-5.6 Sol as formal authors; it proves erdos_471 : ∃ Q : Finset ℕ, IsPrimeFinset Q ∧ HasUnboundedGenerations Q from a distinct-summand form of Vinogradov's theorem developed in the same repository, so it is a formalization of this observation and not an independent proof. It was not built or audited here, so formalized is not listed.

Depends on. No page of this wiki; the only input is Vinogradov's theorem, cited above as classical.