---

Claim. For every coloring of the integers with finitely many colors there are pairwise distinct nonzero integers $a,b,c$ of one color with $1/a=1/b+1/c$; the construction gives positive $a,b,c$. This is the question of Problem 303, proved in Lean 4 as the theorem erdos_303 of the code that Zheng Yuan linked from the site's forum on 21 December 2025. Yuan posted the code in the Problem 330 discussion, writing on behalf of the Seed-Prover team and identifying Problem 303 as the problem the system had proved; the proof was produced by Seed-Prover, an automated theorem-proving system, and the claimant is the submitter, Yuan. A re-proof of the code is the file Erdos303.lean in Boris Alexeev's lean-proofs collection (the third link), which names Seed-Prover, Aristotle, Yuan and Alexeev as its formal authors: the repository's note on the file says that the theorems of Yuan's proof were given to Aristotle, Harmonic's system, to reprove, and that the results were reorganized to shorten the proof.

Submission note. Posted to the site's forum by Zheng Yuan on 21 December 2025:

Hello, I am Zheng Yuan from Seed-Prover. I double check our paper and our proved Erdos problems. This is a typo in our paper since we proved Erdos-303, which is easy. We check the version we searched for 330 is the old version, and we do not prove it. We will update our paper soon. By the way, we don't state we prove any new conjectures (That is our next target.). (Check Erdos-303 here (Note from the moderator: this URL is extremely long, please find a shorter one to replace it with.)

Posted to the site's forum by Boris Alexeev on 21 December 2025:

Over on the forum for [330], Zheng Yuan from Seed-Prover posted this link for Lean code that solves this problem formally. The final statement is from the Formal Conjectures project.

(The site has been updated to address this comment.)

Route. The mathematical rewriting of the code: the finite Ramsey theorem applied to an edge coloring of a complete graph by the colors of the differences gives a monochromatic four-clique whose three consecutive gaps supply positive integers $u<v$ with $u$, $v$ and $u+v$ of one color under an auxiliary coloring; a factorial $N$ divisible by all of them transfers the triple to the denominators $N/(u+v)$, $N/u$, $N/v$, which satisfy $1/a=1/b+1/c$, and a parametrization lemma, $(kyz,\,kz(y+z),\,ky(y+z))$, verifies the pairwise distinctness. The proof was produced independently of Brown and Rödl's paper, and it specializes their reciprocal transfer, $y\mapsto N/y$ with $N$ a common multiple, to the single equation, with the finite Ramsey theorem (Schur's theorem) in place of Rado's theorem and compactness; their argument is on their claim page.

Acceptance. Formalized. This corpus's verification built the file src/latest/ErdosProblems/Erdos303.lean of Alexeev's collection at the pinned commit 8822f7dd of 2026-09-15 (Lean v4.33.0, Mathlib v4.33.0, from the lean-toolchain of src/latest) and checked the axioms of Erdos303.erdos_303, which are exactly propext, Classical.choice and Quot.sound. The repository's comparator challenge ComparatorChallenges/ErdosProblems/Erdos303.lean pins that declaration, and its fingerprint was found identical to the challenge's. The statement was audited clause by clause against the problem's Statement and is exact: for every coloring $\mathcal C:\mathbb Z\to\mathbb Z$ with finite range there are integers $a,b,c$ such that the list $[a,b,c,0]$ has no repeated entry (so $a,b,c$ are pairwise distinct and nonzero), $1/a=1/b+1/c$ holds in the reals with the integers cast, and $a,b,c$ have one color. That is the Formal Conjectures statement with its answer(True) wrapper removed, and it also gives the positive-integer version: color each nonzero integer $x$ by its sign together with the color of $|x|$, and negate a negative triple. The build certifies that file, Alexeev's re-proof of the Seed-Prover lemmas with Aristotle, at the pinned commit; the note on the re-proof is kept in the repository's src/v4.24.0 copy of the file at that commit. Yuan's posted payload was not built: its final theorem is also named erdos_303, and its text contains no sorry, admit or axiom, but no kernel check of it is recorded; its provenance and payload identity are on the source card and its source record. The Formal Conjectures statement file for the problem carries an external-proof annotation pointing to the Problem 303 thread while its own theorem body remains by sorry, so it is not a formalization of this claim. Not reviewed: on that thread Alexeev wrote on 21 December 2025 that the linked code formally solves the problem, and the site's curator, Thomas Bloom, relabeled the problem PROVED (LEAN) and marked the comment as addressed, but the site's commentary credits the proof to Brown and Rödl and the Lean to the Formal Conjectures project without naming Yuan or Seed-Prover, so the relabel is not the curator's acceptance of this claim. Not refereed: there is no journal write-up. Brown and Rödl had already proved the result in 1991, and their accepted claim stands beside this one.