---

Claim. The answer is yes: there is a permutation $a_1,a_2,\ldots$ of the positive integers with $a_k+a_{k+1}$ prime for every $k$. Erdős and Graham report on printed p. 94 of their 1980 monograph that Odlyzko constructed such a permutation, settling the question Segal had posed in 1977; the bibliography entry for the construction is marked unpublished, and no write-up of it has been located. The construction itself is therefore not available to this compilation, and the argument is not described here.

Postings. The only record is the 1980 report by Erdős and Graham; the page is dated to the first day of that year, since the monograph carries only a year. The site's page, present with its PROVED label and its attribution to Odlyzko from the earliest revision in the site's history view (20 October 2025), notes that no reference is given; a thread exchange of 8 October 2025 asked where the proof might be found and reported that it could not be located.

Acceptance. Erdős and Graham, named experts writing in a published monograph, record the construction as settling the question, and the site's curator, Thomas Bloom, accepted that record by labeling the problem PROVED and crediting Odlyzko; those documented acceptances are the reviewed evidence. The construction has not been refereed or read, here or, as far as the records show, anywhere accessible. The two-way infinite variant has a refereed proof by other authors, noted on the problem page as a related result rather than a claim on this question.

Formalization. The file Erdos473.lean in Boris Alexeev's repository lean-proofs, linked above at a pinned commit and added on 17 August 2026, declares itself a formalization of a solution to Erdős Problem 473, naming A. M. Odlyzko as informal author and Codex and GPT-5.6 Sol as formal authors. It proves erdos_473 : ∃ a : ℕ ≃ ℕ+, ∀ n : ℕ, Nat.Prime ((a n : ℕ) + (a (n + 1) : ℕ)) by a graph-theoretic construction: a countable graph in which every finite path can be extended to reach any prescribed vertex has a spanning one-way ray, and the prime-sum graph on the positive integers has that property, shown through clusters of primes and a Siegel-Walfisz lower bound imported from the repository's development for Problem 387. Since Odlyzko's construction has never been located, the formal argument is not known to follow it. The formal-conjectures statement of the problem names this file in its formal_proof attribute. It was not built or audited here, so formalized is not listed.

Depends on. No page of this wiki.