PROVED (LEAN). The site labels the problem PROVED (LEAN) (page last edited 6 January 2026) and credits Barreto and ChatGPT-5.2 for a proof that, for any $0<C_1<C_2$, gives infinitely many triples with $b=n/2$, $a=n/2+O(\log n)$, $C_1\log n<a+b-n<C_2\log n$ and $a!\,b!\mid n!\,(a+b-n)!$; the result is recorded on the claim page Barreto 2026. A separate proof by Carl Pomerance, extending his 2015 method and written after the thread asked him about the AI-generated proof, gives a far larger gap for almost all $n$; published in Integers in 2026, it is on the claim page Pomerance 2026; two later AI-generated proofs posted to the site's thread are on the pending page Pickhardt 2026. The Lean qualifier refers to Aristotle's formalization of the ChatGPT-5.2 argument, posted by Barreto and shortened by Boris Alexeev in his repository of formalized Erdős problems, which this corpus has not built; nothing about the AI-generated proof is refereed, and the site's commentary notes that the statement as printed is ambiguous (see the assessment below). The standing in the frontmatter derives from the claim pages.