🔢 mathematics

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

This paper presents the first fully autonomous AI resolution of Erdős Problem #728, utilizing a combination of GPT-5.2 Pro and the Aristotle system to generate a formal Lean proof demonstrating a logarithmic-gap phenomenon in factorial divisibility through a novel prime-by-prime analysis of binomial coefficients.

Original authors: Nat Sothanaphan

Published 2026-01-27

📖 5 min read🧠 Deep dive

CC BY 4.0

Original authors: Nat Sothanaphan

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

The Big Picture: A Team of AI Mathematicians

Imagine a famous, retired math genius named Paul Erdős who spent his life leaving behind a giant "To-Do" list of unsolved puzzles. One of these puzzles, #728, has sat untouched for decades.

Recently, a team consisting of a super-intelligent AI (GPT-5.2 Pro) and a specialized math-checking robot (Aristotle) finally solved it. They didn't just guess the answer; they built a rigorous, step-by-step proof that a computer can verify is 100% correct. The authors of this paper are simply translating that computer code into a story humans can read.

The Puzzle: The Factorial Balancing Act

The problem asks a question about factorials (numbers like $5! = 5 \times 4 \times 3 \times 2 \times 1$ ).

Imagine you have a massive pile of blocks representing $n!$ . You want to see if you can build two smaller towers, $a!$ and $b!$ , and a third small tower $k!$ , such that the two small towers fit perfectly inside the big one without any blocks left over.

Mathematically, this means: Does $a! \times b!$ divide evenly into $n! \times k!$ ?

The puzzle asks: How big can the "gap" ( $k$ ) be?

If $k$ is tiny, it's easy to fit the blocks.
If $k$ is huge, it's usually impossible.
The trick is to find a "Goldilocks zone" where $k$ is big enough to be interesting, but not so big that the blocks don't fit.

The AI team proved that you can find infinitely many situations where this gap ( $k$ ) is roughly the size of the logarithm of the total number. In plain English: If your total number of blocks is a million, the gap can be around 14. If your number is a billion, the gap can be around 20. It grows very slowly, but it does grow.

The Strategy: The "Carry" Game

To solve this, the mathematicians had to look at the problem through the lens of prime numbers (2, 3, 5, 7, etc.). They used a rule called Kummer's Theorem, which is like a game of "carrying" in addition.

The Analogy: The Overflowing Bucket
Imagine you are adding numbers in a specific language (base $p$ ).

When you add two digits and the result is too big for one slot, you "carry" the extra to the next slot.
The Goal: The AI needed to find a number ( $m$ ) that, when doubled, causes lots of carries (like a bucket overflowing repeatedly).
The Obstacle: At the same time, the AI had to make sure that the numbers immediately following $m$ (like $m+1, m+2...$ ) didn't have any "spikes"—sudden, massive divisibility by a prime that would ruin the balance.

Think of it like walking a tightrope:

The Tightrope (The "Carry" Condition): You need to pick a number that is "carry-rich." When you double it, it should overflow its buckets as often as possible. This creates a "safety net" of divisibility that helps the equation work.
The Spikes (The "Bad" Condition): You must avoid numbers where the next few integers are divisible by huge powers of a prime. These are "spikes" that would knock you off the tightrope.

How They Found the Solution

The AI didn't just pick a random number. It used a counting argument (a statistical strategy):

The Search Area: They looked at a huge range of numbers (from $M$ to $2M$ ).
The Filter: They calculated how many numbers in this range were "bad" (either they didn't carry enough, or they had a spike).
The Result: They proved that the number of "bad" candidates is actually smaller than the total number of candidates in the range.
The Conclusion: Since there are more numbers than "bad" numbers, there must be at least one "good" number left in the pile.

It's like saying: "If you have a jar of 1,000 marbles, and only 900 of them are red (bad), there must be at least 100 blue ones (good) left." The AI proved that for any large enough jar, a "good" marble always exists.

Why This Matters (According to the Paper)

First AI-Only Proof: This is the first time an AI system has autonomously solved one of Erdős's famous problems and produced a formal proof that humans can verify.
The "Logarithmic Gap": They confirmed that the gap between the numbers can be logarithmic. While the paper notes that the gap could potentially be slightly larger (as suggested by mathematician Terence Tao), this proof establishes a solid, guaranteed baseline.
Methodology: The method used (counting carries and avoiding spikes) is similar to techniques Erdős himself used in the past, but applied here to a more complex, moving target.

Summary

The paper is a report on how an AI team solved a 40-year-old math puzzle. They showed that you can always find a specific set of numbers where a complex factorial equation balances perfectly. They did this by treating numbers like buckets that overflow (carries) and proving that you can always find a bucket that overflows just enough to be useful, without spilling too much in the wrong places.

Technical Summary: Resolution of Erdős Problem #728

Problem Statement
The paper addresses Erdős Problem #728, which investigates the maximum possible size of the gap $k := a + b - n$ under the constraint of factorial divisibility:
$a! b! \mid n! (a + b - n)!$
Without additional constraints, trivial solutions exist where $k$ is arbitrarily large (e.g., by taking $a$ and $b$ very large). To make the problem non-trivial, the authors impose the condition that $a$ and $b$ are bounded away from the extremes, specifically $\varepsilon n \le a, b \le (1-\varepsilon)n$ for some $0 < \varepsilon < 1/2$ . The goal is to determine how large $k$ can be relative to $n$ under these constraints.

Methodology and Proof Strategy
The proof proceeds by transforming the factorial divisibility condition into a problem concerning binomial coefficients and $p$ -adic valuations.

Reduction to Binomial Divisibility:
By setting $n = 2m$ , $b = m$ , and $a = m + k$ , the original condition is equivalent to:
$\binom{m+k}{k} \mid \binom{2m}{m}$
This requires showing that for every prime $p$ , the $p$ -adic valuation of the left-hand side is less than or equal to that of the right-hand side:
$\nu_p\left(\binom{m+k}{k}\right) \le \nu_p\left(\binom{2m}{m}\right)$
Valuation Analysis via Kummer's Theorem:
Using Kummer's theorem, $\nu_p\left(\binom{2m}{m}\right)$ is identified with the number of carries occurring when adding $m + m$ in base $p$ . The term $\nu_p\left(\binom{m+k}{k}\right)$ is bounded by the maximum valuation of any term in the consecutive block $m+1, \dots, m+k$ , denoted $V_p(m, k)$ .
The core inequality to satisfy is:
$V_p(m, k) \le \kappa_p(m)$
where $\kappa_p(m)$ is the carry count for $m+m$ in base $p$ .
Prime-by-Prime Analysis:
The authors split the analysis into two regimes based on the size of the prime $p$ relative to $k$ :
- Large Primes ( $p > 2k$ ): In this range, the inequality holds automatically. Since the interval length $k$ is smaller than $p/2$ , at most one number in the block $m+1, \dots, m+k$ can be divisible by $p$ . If a high power $p^J$ divides a term, the base- $p$ digits of $m$ force at least $J$ carries when doubled, satisfying the condition.
- Small Primes ( $p \le 2k$ ): This is the main difficulty. The authors employ a probabilistic counting argument to find an integer $m$ $m$ in a large interval $[M, 2M]$ $[M, 2 M]$ that simultaneously satisfies two conditions for all $p \le 2k$ $p \leq 2 k$ :
  - Carry-Rich: The base- $p$ expansion of $m$ has many digits $\ge \lceil p/2 \rceil$ in the first $L_p$ positions. This forces a high number of carries ( $\kappa_p(m)$ ) when $m$ is doubled.
  - Spike-Free: No integer in the block $m+1, \dots, m+k$ is divisible by an unusually high power of $p$ (specifically, $V_p(m, k)$ is kept below a threshold $J_p + t(M)$ ).
Existence via Union Bound:
The authors define "bad" sets of integers $m$ that fail either the carry condition or the spike condition. Using Chernoff bounds for the distribution of large digits and simple counting for the spike condition, they show that the total measure of these bad sets is strictly less than the size of the interval $[M, 2M]$ . Consequently, a "good" $m$ exists that satisfies the divisibility condition for all relevant primes simultaneously.

Key Results
The paper establishes Theorem 1 (Logarithmic gap window):
For any constants $0 < C_1 < C_2$ and $0 < \varepsilon < 1/2$ , there exist infinitely many triples $(a, b, n) \in \mathbb{N}^3$ such that:

$\varepsilon n \le a, b \le (1-\varepsilon)n$
$a! b! \mid n! (a + b - n)!$
$C_1 \log n < a + b - n < C_2 \log n$

The construction yields a gap $k$ that grows logarithmically with $n$ . The authors note that the current proof yields $k \asymp \log n$ , but the method could potentially be extended to $k = \exp(c\sqrt{\log n})$ with further refinement, though the current writeup focuses on the logarithmic regime.

Significance and Claims

First AI-Resolved Erdős Problem: The authors claim this is the first Erdős problem to be "fully resolved autonomously by an AI system." The system utilized was a combination of GPT-5.2 Pro and the theorem prover "Aristotle" by Harmonic.
Formal Verification: The proof was generated as a formal proof in the Lean theorem prover and subsequently translated into the informal mathematics presented in this writeup.
Methodological Contribution: The work extends previous techniques by Erdős and Pomerance regarding divisors of central binomial coefficients. Unlike prior work that focused on "carry-poor" integers (few carries) or fixed gap sizes, this proof constructs "carry-rich" integers to handle a growing window of size $k \asymp \log n$ .
Independence: The authors note that after their initial work, Carl Pomerance independently derived similar results, and modifications of this argument were used to solve Erdős Problems #729 and #401.

The paper does not claim to solve the problem in its absolute strongest possible form (noting the potential for larger gaps) but asserts the successful resolution of the specific logarithmic gap question posed by Erdős.