Claims

../

2026_01_11_barreto_price: For every r, infinitely many n admit a_1 + a_2 exceeding n by a multiple of log n that grows with r while a_1! a_2! divides n! times the n-th power of the product of the first r primes; proved with GPT-5.2 Pro, Lean by Aristotle.

2026_01_11_sothanaphan: The valuation argument behind the Lean proof of Problem 728, generalized to a density-one theorem, yields the examples Problem 401 asks for; stated with a sketched proof in the appendix of Sothanaphan's arXiv write-up.

---