Erdős Problem #403 — sums of distinct factorials that are powers of 2 #
Problem (Burr–Erdős; [ErGr80, p.79]). Does
2^m = a₁! + a₂! + ⋯ + aₖ! with a₁ < a₂ < ⋯ < aₖ have only finitely many solutions?
Answer: yes (Frankl and Shen Lin, independently, 1976 — both proofs unpublished;
Lin's was a Bell Labs internal memorandum, "On Two Problems of Erdős Concerning Sums of
Distinct Factorials"). The largest solution is 2⁷ = 2! + 3! + 5! = 128.
Because the original proofs are lost to the literature, this is a reconstruction, not a
transcription. The final proof (in Erdos403.Sharp) works in the factorial number system: a sum of
distinct factorials is exactly a factorial-base numeral with all digits ≤ 1, and for every
m ≥ 8 both 2^m and 2^m − 1 carry a digit ≥ 2 at some index ≤ 11 — a finite, fixed-modulus
(12!) check. Both erdos_403_finite and erdos_403_sharp are sorry-free and kernel-pure.
- This file: the core definition
factSum, the extremalwitness, and the size sandwich. Erdos403.FactBase: the factorial-number-system digit machinery.Erdos403.Sharp: the headline theorems.Erdos403.Superseded: an earlier, unused 2-adic valuation approach, preserved for the record.
A "sum of distinct factorials" is modelled by a Finset ℕ of indices (distinctness of the aᵢ is
automatic). Note 0! = 1! = 1, so e.g. {0,1} sums to 2.
The sum of distinct factorials indexed by S: ∑_{a ∈ S} a!.
Equations
- Erdos403.factSum S = ∑ a ∈ S, a.factorial
Instances For
The size sandwich #
For nonempty S with top element M = max' S: M! ≤ factSum S ≤ 2·M!. The lower bound (the top
factorial is one of the summands) is what the finiteness argument in Erdos403.Sharp uses.
The partial factorial sum is bounded by the top factorial: ∑_{a<n} a! ≤ n!. Tight at
n = 0,1,2.