---

The claim. The file src/v4.29.1/ErdosProblems/Erdos493.lean of Boris Alexeev's public repository plby/lean-proofs proves, as erdos_493_aristotle and again as erdos_493_chatgpt, that there are $k$ and $N$ such that every integer $n\ge N$ equals $\prod_{i<k}a_i-\sum_{i<k}a_i$ for some $a_0,\ldots,a_{k-1}\in\mathbb Z$ with every $a_i\ge2$: the formal-conjectures statement of Problem 493 without its answer(True) wrapper. Both proofs take $k=2$, $N=0$ and the pair $2$, $n+2$. This answers the question yes by the same construction as Seamans's identity, which the site credits; the two are recorded apart because the file names no informal author and so presents itself as an independent proof.

Provenance. The claimant is Boris Alexeev, who published the file and posted the Aristotle proof in the thread's first comment of 27 December 2025, writing that it was generated by the prover Aristotle and that ChatGPT had also solved the problem in Lean, and opening with a priority note that ByteDance's Seed AI4Math group had reported Seed-Prover 1.5 as having solved the problem, a proof Alexeev had not seen. The file's header, at the pinned revision of 24 June 2026, calls it a formalization of a solution to the problem and lists Seed-Prover 1.5, Aristotle, ChatGPT and Zheng Yuan as its formal authors, naming no informal author; the repository's index page for the problem names no one either. The file carries two proofs of the statement, one attributed to Aristotle and one to ChatGPT, and a closing comment recording #print axioms for the first as propext, Classical.choice and Quot.sound. The formal-conjectures file ErdosProblems/493.lean carries a formal_proof attribute naming this file on the repository's main branch, not a fixed commit. The file was neither built nor audited in this corpus: no kernel credit is claimed and formalized is not listed as evidence. The site's Lean mark refers to this file, and the community database records the problem "proved (Lean)" from 27 December 2025.

Acceptance. None listed. The site's curator credits the identity to Seamans in the problem's commentary and does not credit this file; the Lean mark on the site's label is a catalog mark that no comment or commentary ties to a review of the file. The construction itself is checked by the arithmetic on Seamans's page.

Depends on. No page of this wiki.