---

Claim. The answer to Problem 493 is yes, with $k=2$. For every integer $n\ge0$ take $a_1=2$ and $a_2=n+2$, both at least $2$; then

$$a_1a_2-(a_1+a_2)=2(n+2)-(n+4)=n.$$

So every nonnegative integer, not only every sufficiently large one, has the required form. The site's commentary records this observation and credits it to Eli Seamans, and the problem page thanks Seamans by name.

Date. The commentary carries no date, and no posting by Seamans was found. An archived capture of the site's page of 21 July 2024 already carries the credit, under the label SOLVED, so the observation is no later than that date; this page is named by it, the earliest dated record of the credit. The community database listed the problem as proved before December 2025 and has recorded it as proved (Lean) since 27 December 2025, the day an AI-generated Lean proof of the same identity was posted on the thread (below).

Qualification. Erdős attributes the question to Schinzel, and the site's curator notes that Schinzel probably intended an extra constraint that the 1961 source (card) does not record; one suggestion on the thread is that the question was meant for every $k\ge2$ at once. The claim settles the question as the catalog states it and nothing about such variants.

Lean proof. A Lean proof of the same construction, generated by AI systems and posted by Boris Alexeev on the problem's thread on 27 December 2025, is the pending claim Alexeev's AI-generated Lean proof. Its file names no informal author, so it is recorded as an independent proof with its own page rather than as a formalization link here; this repository has not built it, and the site's Lean mark refers to it.

Acceptance. Reviewed: the site's curator, Thomas Bloom, who is independent of the claimant, labels the problem proved and credits Seamans's observation in the problem's commentary. The identity is checked by the two lines above. Not refereed: the observation has no publication.

Depends on. No page of this wiki.