Resolution of Erdős Problem #728: a writeup of Aristotle's Lean proof

Abstract We provide a writeup of a resolution of Erd ̋os Problem #728; this is the first Erd ̋os problem (a problem proposed by Paul Erd ̋os which has been collected in the Erd ̋os Problems website [3]) regarded as fully resolved autonomously by an AI system. The system in question is a combination of GPT-5.2 Pro by OpenAI and Aristotle by Harmonic, operated by Kevin Barreto. The final result of the system is a formal proof written in Lean, which we translate to informal mathematics in the present writeup for wider accessibility. The proved result is as follows. We show a logarithmic-gap phenomenon regarding factorial divisibility: For any constants 0 < C1 < C2 and 0 < ε < 1/2 there exist infinitely many triples (a, b, n) ∈N3 with εn ≤a, b ≤(1 −ε)n such that a! b! | n! (a + b −n)! and C1 log n < a + b −n < C2 log n.

The argument reduces this to a binomial divisibility m+k k | 2m m and studies it prime-byprime. By Kummer’s theorem, νp 2m m translates into a carry count for doubling m in base p. We then employ a counting argument to find, in each scale [M, 2M], an integer m whose base-p expansions simultaneously force many carries when doubling m, for every prime p ≤2k, while avoiding the rare event that one of m + 1, . . . , m + k is divisible by an unusually high power of p. These “carry-rich but spike-free” choices of m force the needed p-adic inequalities and the divisibility. The overall strategy is similar to results regarding divisors of 2n n studied earlier by Erd ̋os [7] and by Pomerance [10].

Introduction. Erd ̋os Problem #728 [3] asks how large the gap k := a + b −n can be, assuming the factorial divisibility a! b! | n! k!.

Equivalently, writing N = a + b, this asks for large k such that N k N a ∗natsothanaphan@gmail.com The qualitative feature exploited in the proof is that the right-hand side contains the full factorial k!. For a fixed prime p, this contributes the term νp(k!), which grows like k/(p −1) and thus can be arranged to dominate sporadic p-adic contributions coming from the factor (m + i) in a consecutive block. After an explicit change of variables, the problem reduces to proving the binomial divisibility m + k k Theorem 1 (Logarithmic gap window). Fix 0 < C1 < C2. Let 0 < ε < 1/2. There exist infinitely many (a, b, n) ∈N3 with εn ≤a, b ≤(1 −ε)n such that a! b! | n! (a + b −n)! and C1 log n < a + b −n < C2 log n.

Related work. and provenance Erd ̋os Problem #728, as stated in [3], asks how large the gap a + b −n can be under the factorial divisibility a! b! | n! (a + b −n)!.

This problem originally appears in [8].

The proof strategy is closely related to several divisibility results for central binomial coefficients, usually governed by Kummer’s carry interpretation of p-adic valuations. Erd ̋os’ problem Aufgabe 557 in Elemente der Mathematik [7] concerns the stronger divisibility a! b! | n! (i.e. the case k = 0). Erd ̋os proved an upper bound a + b < n + O(log n) in this setting, and observed that this is sharp up to the constant. The published solutions show a strong “almost all n” statement: for a sufficiently small absolute constant C > 0 and a = ⌊C log n⌋, one has for almost all n the interval product divisibility (n + 1) · · · (n + a) 2n n This is close in spirit to the present proof. Indeed, after rewriting m+k k = (m + 1) · · · (m + k)/k!, our target divisibility m+k k | 2m m is a “binomial-coefficient” analogue of such interval-product divisibilities. The paper of Erd ̋os–Graham–Ruzsa–Straus [8] which contains the present question itself studies the distribution of prime factors of 2n n , quantifying, among other things, how small primes contribute high powers and how primes are avoided. We do not use specific results from [8]. Pomerance [10] studies questions about divisors of the central binomial coefficient 2n n . One of his main theorems shows that for each fixed k ≥1, the set of n for which n + k divides 2n n has asymptotic density 1 ([10, Theorem 2]). The methods in [10] exploit Kummer’s theorem and the idea that base-p digit patterns behave “randomly.” Our argument is in the same vein, but differs in two key respects: (i) we treat a growing window length k ≍log n rather than a fixed k, and (ii) we work with a structured divisor m+k k of 2m m rather than a single linear factor n + k. After Pomerance’s paper, there has been further progress on related divisibility questions for 2n n , in several directions. Ford and Konyagin [9] prove that for each fixed l∈N the set of n such that nl| 2n n has a positive asymptotic density cl, and they obtain an asymptotic formula for cl as l→∞. They also show that #{n ≤x : (n, 2n n ) = 1} ∼cx/ log x for an explicit constant c. Croot, Mousavi, and Schmidt [6] study a problem motivated by Graham’s conjecture on gcd 2n n , 105 . They show that for any fixed r ≥1 and any 0 < ε < 1/(20r2), there is a threshold p0(r, ε) such that for any distinct primes p1, . . . , pr ≥p0(r, ε) there exist infinitely many n for which νpj 2n n ≤ε log n log pj (j = 1, . . . , r).

Method. 3 Reduction to a valuation inequality Let m ≥1 and k ≥1 be integers and set n := 2m, b := m, a := m + k. (1) Then b = n/2 and a + b −n = k. We will choose a large scale M and search for some m ∈[M, 2M]. We set k := ⌊c log M⌋, (2) where c > 0 is a constant. In the final step (proof of Theorem 1) we choose any c ∈(C1, C2) to obtain the two-sided logarithmic window.

Thus, the main work is the factorial divisibility in Theorem 1. With n = 2m, b = m, a = m+k, the factorial divisibility becomes (m + k)! m! | (2m)! k!. (3) Lemma 1 (Binomial reformulation). For all m, k ∈N, (m + k)! m! | (2m)! k! ⇐⇒ m + k k 2m m Proof. Immediate.

Fix a prime p. Define κp(m) := νp 2m m , Wp(m, k) := νp Podk i=1(m + i) , Vp(m, k) := max 1≤i≤k νp(m + i).

Because m+k k = Podk i=1(m + i) k! , we have the exact identity m + k k = Wp(m, k) −νp(k!). (4) Lemma 2 (Valuation reduction). For all primes p and all m, k, m + k k ≤κp(m) ⇐⇒ Wp(m, k) ≤κp(m) + νp(k!).

Proof. Immediate from (4).

Thus, it suffices to show Wp(m, k) ≤κp(m) + νp(k!) for every prime p.

Remark 2. The dominant contribution to Wp(m, k) for small primes is typically ∼k/(p −1), but (4) subtracts νp(k!), which has the same main term. This makes it easier to establish the required inequality.

Lemma 3 (Kummer’s theorem). For a prime p, κp(m) equals the number of carries when adding m + m in base p.

We now obtain an intermediate bound which is useful in reducing the problem to a simpler inequality.

Lemma 4 (Interval valuation bound). For every prime p and all m, k, Wp(m, k) ≤νp(k!) + Vp(m, k).

Proof. For j ≥1 let Nj := #{1 ≤i ≤k : pj | (m + i)}.

Then Wp(m, k) = k X i=1 νp(m + i) = X j≥1 Nj, since each term (m + i) contributes 1 to Nj. Among k consecutive integers, the number of multiples of pj is at most ⌈k/pj⌉, so Nj ≤ k (j ≥1).

Let J := ⌊logp k⌋, so pJ ≤k < pJ+1. For 1 ≤j ≤J we have ⌈k/pj⌉≤⌊k/pj⌋+ 1. For j ≥J + 1 we have pj > k, hence among m + 1, . . . , m + k there is at most one multiple of pj, so Nj ≤1. Finally Nj = 0 for all j > Vp(m, k). Therefore Wp(m, k) = X j≥1 Nj ≤ J X j=1 + 1 + Vp(m,k) X j=J+1 1 = J X j=1 + Vp(m, k).

By Legendre’s formula, νp(k!) = PJ j=1⌊k/pj⌋. This establishes the claim.

Combining Lemma 2 with Lemma 4, it is enough to show Vp(m, k) ≤κp(m) for every prime p.

4 Prime-by-prime analysis via carries We now analyze the inequality Vp(m, k) ≤κp(m) in ranges p > 2k and p ≤2k.

4.1 The range p > 2k In this range, the desired inequality holds for free.

Lemma 5 (Large prime lemma). If p is prime and p > 2k, then for all m, κp(m) ≥Wp(m, k) = Vp(m, k).

Proof. Because p > k, at most one of the k integers m + 1, . . . , m + k can be divisible by p; more generally, for each j ≥1, at most one of m + 1, . . . , m + k can be divisible by pj. Consequently, Wp(m, k) = Vp(m, k). If Vp(m, k) = 0 then the claim is trivial. Otherwise let J := Vp(m, k) ≥1 and pick i ∈{1, . . . , k} such that pJ | (m + i). Write m + i = pJu with p ∤u. Since i ≤k < p/2, in base p, the lowest J digits of m agree with those of pJ −i. But pJ −i has base-p expansion with the lowest digit equal to p −i and the next J −1 digits equal to p −1. All these digits are ≥(p + 1)/2. In the addition m+m in base p, a digit a ≥(p+1)/2 forces a carry at that position regardless of incoming carry. Therefore the lowest J digit positions contribute at least J carries. By Kummer’s theorem (Lemma 3), κp(m) equals the total number of carries, so κp(m) ≥J.

4.2 The range p ≤2k We will enforce a carry lower bound by inspecting the first few base-p digits of m. To make a counting argument on m ∈[M, 2M] work cleanly, we choose a digit depth Lp so that pLp is slightly smaller than M. Concretely, set η := 1 10, Lp := (1 −η) log M log p Among residues modulo pLp, the base-p digits are uniform in {0, 1, . . . , p −1}. A digit is at least ⌈p/2⌉with probability θ(p) := 2, p = 2, p−1 2p , p ≥3, so the expected number of large digits among the first Lp digits is μp := Lp θ(p).

4.2.1 Carry lower bound and spike control Let Xp(m) be the number of the first Lp base-p digits of m which are ≥⌈p/2⌉.

Lemma 6 (Forced carries from large digits). For every prime p and every m, κp(m) ≥Xp(m).

Conclusion. 5 Completion of the proof We now complete the argument and prove the logarithmic window result.

Proof of Theorem 1. Choose any constant c with C1 < c < C2. For each sufficiently large M, set k = ⌊c log M⌋and apply Lemma 14 to obtain an m ∈[M, 2M] satisfying the small-prime carry and no-spike conditions for all primes p ≤2k. Fix such an m. For primes p ≤2k, the good-m conditions imply Vp(m, k) ≤κp(m). For primes p > 2k, Lemma 5 implies Vp(m, k) ≤κp(m). Therefore, using Lemma 4, Lemma 2, and Lemma 1, this implies the factorial divisibility a! b! | n! (a + b −n)! for the triple n := 2m, b := m, a := m + k.

It remains to verify the window bounds. Recall k = a + b −n. Since m ∈[M, 2M], log n = log M + O(1) as M →∞. So k/ log n →c as M →∞. Hence for large M, C1 log n < k < C2 log n.

Letting M →∞along an infinite sequence yields infinitely many triples.