Claims

../

1976_01_01_lin: Only finitely many powers of two are sums of distinct factorials, the largest being 2^7 = 2! + 3! + 5!; shown by Lin in a Bell Laboratories memorandum and independently by Frankl, as the problem's source reports.

2026_06_18_axiommath: A Lean 4 proof, produced by the AxiomProver system and published in the AxiomMath repository, shows that 2^m is a sum of distinct positive factorials exactly for m in {0, 1, 3, 5, 7}, with the five solutions listed.

---