---

Claim. The answer is yes, by the argument of the sibling page Mrazović and Kovač: Vinogradov's theorem in its distinct-primes form gives an $N$ such that every prime above $N$ is a sum of three distinct smaller primes, so $Q_0$ equal to the set of primes at most $N$ generates every prime.

Postings. The site's commentary records that Noga Alon made the observation independently of Mrazović and Kovač; the communication 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. There is no paper and no thread comment by Alon.

Acceptance. The site's curator, Thomas Bloom, wrote the argument into the commentary of Problem 471, labeled the problem PROVED and thanks Alon on the page; that documented acceptance by a curator who had no part in the result is the reviewed evidence. Nothing was reviewed here.

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 on the sibling page as classical.