---

Claim. Collin Yuanjie Ren's Lean theorem erdos_324_low_degree_and_quartic states that no $f\in\mathbb Z[X]$ with degree at most two, or with $f=X^4$, makes $(a,b)\mapsto f(a)+f(b)$ injective on the pairs of natural numbers $a<b$. The injectivity clause is the one of the formal-conjectures statement of Problem 324, so any polynomial answering the problem has degree at least three and differs from $X^4$. For a quadratic the proof writes down an explicit colliding pair of pairs; for $X^4$ it uses Euler's identity $59^4+158^4=133^4+134^4$.

Covers. Polynomials of degree at most two, and $X^4$. Both facts were known before: the site's commentary calls the quadratic case easy and the quartic case classical, and Dubickas and Novikas prove the degree one and two cases in their introduction (their claim page).

Depends on. No page of this wiki.

Standing. Claimed. The development was submitted, in a commit of 16 September 2026, as a prize-intake package that claims no mathematical novelty; its README says the Lean proof was prepared with the assistance of Claude Code (Claude Fable 5.1 orchestration, Claude Opus 5 implementation) and reports a local build whose axiom audit prints only propext, Classical.choice and Quot.sound. The development is not a formalization of a named claimant's paper, so it has its own page. This corpus has not built or audited it, so no formalized evidence is listed.