Problem detail · source-aware
VibeMathed reports this item as resolved. VibeMath preserves that report as a source assertion and has not independently authored a plain-language mathematical explanation.
Whether there are infinitely many integers $a, b, n$ with $a, b \ge \varepsilon n$ such that $a!\cdot b!$ divides $n!\cdot(a+b-n)!$ while $a+b$ exceeds $n$ by more than $C\cdot\log n$.
The source statement is reproduced for indexing with attribution. Mathematical correctness requires domain-expert or mechanical review. VibeMath has not independently audited statement fidelity, correctness, priority, or novelty.
Aristotle (Harmonic's Lean-based prover) and GPT-5.2 Pro produced a fully autonomous, Lean-verified proof. Regarded by the erdosproblems.com maintainers as the first Erdős problem resolved autonomously by AI systems, about three months before the more widely covered #1196 result.
Provider: Harmonic / OpenAI · Prompt public: unknown · Independence: unknown
Machine-checked end to end in the Lean proof assistant - every logical step formally verified, not just human-reviewed. Written up formally by Nat Sothanaphan.
Correctness: supported · statement fidelity: audited · peer review: none
VibeMathed reports this item as resolved. VibeMath preserves that report as a source assertion and has not independently authored a plain-language mathematical explanation.
Source-reported tools: argument.
Independent: unknown · difference confidence: 0
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.