---

Claim. The answer to Problem 405 is yes, with the complete list. Yu and Liu prove that for an odd prime $p$ and positive integers $a,k$ the equation

$$(p-1)!+a^{p-1}=p^k$$

holds only for $(p,a,k)=(3,1,1)$, $(3,5,3)$ and $(5,1,2)$, that is

$$2!+1^2=3,\qquad 2!+5^2=3^3,\qquad 4!+1^4=5^2 .$$

The list is finite, so the question is answered; the finiteness itself, with an effective bound on every solution, was proved earlier by Brindza and Erdős on the claim page Brindza and Erdős 1991, and Yu and Liu's title calls their result the complete resolution of the problem. The library holds no copy of the paper; the statement is taken from the site's problem page and from the formal-conjectures record of the problem, whose variant erdos_405.variants.yu_liu states the same three triples.

Formalization. The Lean file Erdos405.lean in Boris Alexeev's repository of Lean proofs declares itself a formalization of a solution to the problem, with Brindza, Erdős, Yu, Liu and Maohua Le as its informal authors and the AI systems Codex and GPT-5.6 Sol as its formal authors. Its theorem erdos_405 states that every solution with $p$ an odd prime is one of the three triples above, the statement of this page, and its header credits the three triples to Yu and Liu and to Le together. Le's paper, Publ. Math. Debrecen 48 (1996), no. 1-2, 145--149, determines the same three solutions independently and is recorded on its own claim page; the zbMATH review of the present paper (Zbl 0886.11018) notes Le's similar result. The file was added on 2026-08-17 and the link pins the last commit that touched it at its path; the file's text at that commit contains no sorry. The formal-conjectures statement file names no formal proof. This corpus has not built or audited the file, so the page lists no formalized evidence.

Acceptance. The site's curator, T. F. Bloom, marks the problem proved and credits this paper for the list of solutions, which the page lists as reviewed. The paper is K. Yu and D. Liu, A complete resolution of a problem of Erdős and Graham, Rocky Mountain J. Math. 26 (1996), no. 3, 1235--1244, a refereed journal, listed as refereed. The page is dated by the publisher's record, which gives 1996-09-01 for the issue.