---

Claim. The answer to Problem 403 is yes: the equation $2^m=a_1!+\cdots+a_k!$ with $a_1<\cdots<a_k$ has only finitely many solutions, and the largest is

$$2^7=128=2!+3!+5! .$$

The site credits the result to S. Lin, On two problems of Erdős concerning sums of distinct factorials, a Bell Laboratories internal memorandum, cited as [Li76]. The problem's source, p. 79 of Erdős and Graham's 1980 monograph (Erdős and Graham 1980), states that Burr and Erdős asked the question, that $2^7$ seemed the largest solution, and that Frankl, in a personal communication the monograph cites as [Frank (76)], and independently Lin proved it the largest. Lin's memorandum shows more: $2^{254}$ is the largest power of $2$ that can divide a sum of distinct factorials one of which is $2!$, and $3^m$ is a sum of distinct factorials only for $m\in\{0,1,2,3,6\}$. With the $a_i$ positive integers, as the Lean statements fix them, the complete list of solutions of the equation is $2^0=1!$, $2^1=2!$, $2^3=2!+3!$, $2^5=2!+3!+4!$ and $2^7=2!+3!+5!$, and the Lean classification on the AxiomProver page proves the list complete; if $a_1=0$ is admitted, six further solutions, none above $2^7$, appear, and the problem page lists them. The library holds no copy of the memorandum; its results are taken from the monograph and the site.

Posting and date. The memorandum has no known public posting; the site's problem page (last edited 28 October 2025) is the only link. The monograph's bibliography prints it as [Lin (76)], a Bell Laboratories internal memorandum of 1976; the site's key agrees, while its citation prints 1960, a misprint the formal-conjectures file copies. This page takes the year 1976 from the monograph and, knowing no month, is dated to the first of January 1976. Frankl's independent proof is the personal communication the monograph cites as [Frank (76)], with no written record, so it is disclosed here and has no page of its own.

Depends on. No page of this wiki.

Acceptance. Thomas Bloom, the site's curator, marks the problem proved and credits Frankl and Lin on the problem page; the community database records the problem as proved with a Lean proof, a status dated 21 June 2026, the Lean proof being the independent classification recorded on the AxiomProver page. The memorandum was not refereed, so no refereed evidence is listed; the acceptance rests on the curator's documented credit and the source's report.