Erdős Problem #650 solved exactly, f(m) = min(m, ⌈2√m⌉), with a strategy proposed by ChatGPT and a Lean proof by Aristotle; first Justin Sun Prize awards in October

Your AI and this story

Key facts

• Paper: ‘Optimal bounds for an Erdős problem on matching integers to distinct multiples’, arXiv 2603.28636 (math.CO, math.NT), submitted 30 March 2026, 8 pages; Wouter van Doorn, Yanyang Li, Quanyu Tang
• Problem (paper): f(m) is the largest integer such that for every set A of m positive integers and every open interval I of length 2a_m there are at least f(m) disjoint pairs (a, b) with a ∈ A dividing b ∈ I. Result: f(m) = min(m, ⌈2√m⌉) for all m
• History (erdosproblems.com/650): Erdős and Surányi (1959) proved f(m) ≥ √m; Erdős and Selfridge gave f(m) ≤ 2⌈√m⌉; GPT 5.4 Pro, prompted by He, Li and Tang, proved f(m) ≤ ⌈2√m⌉, and GPT 5.4 Pro with Aristotle gave a matching lower bound; the site lists the problem as solved by [VLT26]
• AI disclosure (abstract): ‘The proof was obtained through an AI-assisted workflow: the proof strategy was first proposed by ChatGPT, and the detailed argument was subsequently made fully rigorous and formally verified in Lean by Aristotle. The exposition and final proofs presented here are entirely human-written.’
• The problem’s formal statement is in Google DeepMind’s Formal Conjectures repository (ErdosProblems/650.lean)
• Justin Sun Prize (announced Geneva, Oct 5, 2026; carried as TRON-commissioned sponsored content by The Block and Cointelegraph): van Doorn, Tang and Li are the program’s ‘first confirmed awards’, for six Erdős problems: #650; #369, #457 and #469 (van Doorn, Lean-checkable proofs); #1044 (Tang); #1196 (Tang and Li within a wider team). Paid in USDT on TRON or USDC on Ethereum; no amounts or judges named
• Prize site (hejustinsun.com/prize): motto ‘Quod probatur, solvitur’; accepts complete Lean proofs, solutions without Lean, or previously catalogued work; no distinction between human and AI contributors