Problems/Erdos Problem #728

Erdos Problem #728

Erdos Problem #728
Number TheorySOLVED
Year
1975
Difficulty
*****
Solved by
GPT-5.2 Pro + Aristotle (Harmonic) (2026)

Statement

How large can the gap k = a + b - n be, given that a!b! divides n!k!?

a! b!∣n! (a+b−n)!withC1log⁡n<a+b−n<C2log⁡na!\, b! \mid n!\, (a+b-n)! \quad\text{with}\quad C_1 \log n < a+b-n < C_2 \log n

About this Problem

The FIRST Erdos problem fully resolved autonomously by AI. Proved by GPT-5.2 Pro (OpenAI) + Aristotle (Harmonic), operated by Kevin Barreto, with a formal Lean proof. The argument reduces to a binomial divisibility and uses Kummer's theorem to translate into carry counts in base-p expansions. A "carry-rich but spike-free" counting argument completes the proof.

AI Contributions

Full SolutionLeanJan 6, 2026

First Erdos problem fully resolved autonomously by AI. Lean proof produced.

Tools: GPT-5.2 Pro, Aristotle (Harmonic)

About the Lean 4 Prover

Lean 4 is a theorem prover and programming language. When a proof compiles in Lean, it is mathematically certain to be correct — the type checker verifies every logical step. This is the gold standard for formal verification.

Our platform uses fal.ai serverless compute to run Lean verification, and Gemini to generate proof strategies that are then formally checked. ShinkaEvolve provides the evolutionary backbone for automated mathematical discovery.

Mathematical Art

Generate a unique AI illustration of this problem using fal.ai FLUX.

Connected Constellations

Number TheorySOLVED
Erdos-Kac Theorem