{
  "annotation_id": "e1a820c7-6a0f-4750-816e-ac440f64fd31",
  "date_created": "2026-02-17T05:53:12.050000Z",
  "date_modified": "2026-02-17T05:53:12.050000Z",
  "file_hash": "61af148a97ea4700faacd68983e1af0ab64d4fbeb6a59d6b0ac9413d6de47957",
  "private": false,
  "record": {
    "abstract": "We provide a writeup of a resolution of Erd\\H{o}s Problem #728; this is the first Erd\\H{o}s problem (a problem proposed by Paul Erd\\H{o}s which has been collected in the Erd\\H{o}s Problems website) 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.\n  The proved result is as follows. We show a logarithmic-gap phenomenon regarding factorial divisibility: For any constants $0\u003cC_1\u003cC_2$ and $0 \u003c \\varepsilon \u003c 1/2$ there exist infinitely many triples $(a,b,n)\\in\\mathbb N^3$ with $\\varepsilon n \\le a,b \\le (1-\\varepsilon)n$ such that \\[ a!\\,b!\\mid n!\\,(a+b-n)!\\qquad\\text{and}\\qquad C_1\\log n \u003c a+b-n \u003c C_2\\log n. \\] The argument reduces this to a binomial divisibility $\\binom{m+k}{k}\\mid\\binom{2m}{m}$ and studies it prime-by-prime. By Kummer\u0027s theorem, $\\nu_p\\binom{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\\le 2k$, while avoiding the rare event that one of $m+1,\\dots,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 $\\binom{2n}{n}$ studied earlier by Erd\\H{o}s and by Pomerance.",
    "arxiv_id": "2601.07421",
    "authors": [
      "Nat Sothanaphan"
    ],
    "categories": [
      "math.NT"
    ],
    "license": "http://creativecommons.org/licenses/by/4.0/",
    "title": "Resolution of Erd\\H{o}s Problem #728: a writeup of Aristotle\u0027s Lean proof",
    "url": "https://arxiv.org/abs/2601.07421",
    "version": "v1"
  },
  "schema_id": "dorsal/arxiv",
  "source": {
    "execution_id": "4b753640-1131-4bd8-b0ed-b14bccf08a43",
    "id": "arXiv Dataset",
    "type": "Model",
    "variant": "snapshot-2026-01-17",
    "version": "0.1.0"
  },
  "user_id": 1000002
}