AIProofWatch
← Archive
Importance: notable
VerificationAuthor claimAccessible artifact / proof
partial resultai assisted

Erdős #728: an AI-assisted factorial-divisibility proof and human writeup

Sothanaphan’s writeup reports infinitely many factorial-divisibility triples with a+b−n in any prescribed positive logarithmic window, while a and b remain bounded away from 0 and n.

Sources for this record

What was already known

The writeup compares the growing logarithmic-window statement with earlier fixed-shift binomial divisibility results.

What changed and why it matters

A concrete number-theoretic result with explicit provenance and a human-readable reconstruction of the Lean argument.

The AI contribution

GPT-5.2 Pro and Aristotle were operated by Kevin Barreto; a human author translated the formal proof into an explanatory paper.

Limitations

Related literature and subsequent refinements affect novelty and attribution. This is not a claim of sole AI priority. AIProofWatch has not compiled the original formal development.

Verification evidence

Evidence labels show what supports the claim. Importance rates its impact if correct.

Author claim

Version 5 states the theorem and provenance.

Accessible artifact / proof

Human-readable writeup of the Lean argument; formal correspondence is discussed in the paper.

Correction and publication history