Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Claim. The answer to Problem 399 is no: the equation has a solution with , and , namely
Jonas Barfield found it, as the site's problem page records. The bases are not coprime, , and the solution factors as with ; this is consistent with what was known, since Erdős and Obláth had excluded solutions only for coprime with , and the exponent here is . One witness disproves the universal statement, so the claim is the whole problem.
Posting. The site's problem page credits Barfield with the solution; no thread post, proof claim or manuscript carrying it is known. The archived copy of the site's page of 7 April 2025 already labels the problem SOLVED and gives the solution, while the copy of 7 November 2024 shows it OPEN without it, so the solution was public by 7 April 2025; the page is dated by that record, and the exact date of the finding is not recorded. The community database records the problem as disproved (its entry last updated 4 February 2026) and as formalized (last updated 12 January 2026); those are the dates of the entry's last changes, not of the finding.
Formalization. The formal-conjectures file for the problem, linked above at
the commit that added it (12 January 2026), proves its own statement
erdos_399 : answer(False) ↔ ¬∃ n x y k, … by supplying the witness
and checking it with decide; the commit that added it records
Codex's assistance, and the version of 18 September 2026, also linked above,
says in its docstring that it was formalized in Lean by Lu using Codex. This is
a proof inside the formal-conjectures repository, not a bare statement, which is
why it is linked here. This corpus has not built or audited it, so it is not
listed as evidence.
Depends on. No page of this wiki.
Acceptance. Thomas Bloom, the site's curator, marks the problem disproved and credits Barfield's solution on the problem page, recording the formalization in the site's label; the community database records the problem as disproved with a Lean proof. There is no refereed write-up; the acceptance rests on the curator's documented review, and the arithmetic of the witness is checked by hand above.