Research / Jan 2026

Divisibility between products of factorials (Erdős #728)

What is the exact statement and scope of the reported resolution of Erdős problem #728? See the linked paper; an elementary explainer is still needed.

Model / AI: GPT-5.2 Pro, Aristotle

machine-checked

Jan 2026

Divisibility between products of factorials (Erdős #728)

Model / AI: GPT-5.2 Pro, Aristotle

machine-checked

GPT-5.2 Pro plus Harmonic's Aristotle, operated by Kevin Barreto, produced a Lean proof, billed as the first Erdős problem fully resolved autonomously by an AI system; written up in prose by Nat Sothanaphan.

Source review pending. Imported from the original notes; linked claims and artifacts have not been re-audited in this restructuring.

Paper — Erdős Problem #728