Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Claim. In the game of Problem 872, with Prolonger moving first, Shortener has a strategy that ends the game within moves. For any the game therefore cannot be guaranteed to last moves for all large , and the problem's final question has the answer no under that convention. The strategy was found by GPT-5.2 Pro at Liam Price's prompting; Price posted the write-up on the problem's discussion thread on 14 February 2026 as an Overleaf document and added a PDF copy on 15 February 2026. A comment of Xiao Hu on 17 February 2026 refers to the write-up's Lemma 4.1 and its auxiliary set of odd numbers, and improves the saving from to by taking to be the odd numbers in , and in an edit to by taking the odd numbers in not divisible by : the multiples , and of elements of in the upper half of the board are then distinct, so the lemma extends and the rest of the argument is unchanged.
Submission note. Posted to the site's forum by Liam Price on 14 February 2026:
GPT-5.2 Pro appears to have determined a strategy that disproves the last question on the assumption the Prolonger starts first, and can be viewed here. After a quick literature review, ChatGPT Deep Research did not appear to locate anything directly resolving aspects of this problem, but does appear to locate literature on related things. I have attempted formalising the result but have ran into some issues; will keep trying.
Covers. The second displayed question, whether the game can be guaranteed to last moves, answered in the negative when Prolonger moves first. It does not cover the first displayed question, the threshold, nor the order of the guaranteed length , nor the convention in which Shortener moves first. The pending partial claim [[problems/divisors/E0872/claims/2026_07_24_buddhdev|Buddhdev's sublinear bound]] asserts , which would answer both displayed questions and supersede the constant.
Standing. Thomas Bloom, the site's curator, states in the problem's
remarks (page last edited 24 April 2026) that GPT-5.2 Pro, prompted by
Price, has shown that the final question has a negative answer, Shortener
guaranteeing at most moves when Prolonger goes
first, and refers to the comment section for the refined constant. The site
labels the problem OPEN, so the remark is commentary, not acceptance. The
write-up is not refereed, no arXiv posting of it is recorded, and this corpus
has not built the Lean proof below, so the claim is claimed.
Lean proof on the thread. On 8 May 2026 a thread comment by Pommeret
(post 6333) gives a Lean 4 proof of the upper bound, written by
Aristotle and refined with Aristotle and Claude-Opus-4.7, published as a
permalink into the live Lean editor rather than as a repository. To avoid
full game trees it restricts the moves of Shortener only, which a later
comment notes still bounds the value of the game. It is not a formalization
of the problem's formal-conjectures game definition, and this corpus has not
built it, so no formalized evidence is listed; a comment of 21 May 2026
calls the result accepted as correct with the formalization incomplete.
Claimant and system. Liam Price posted the result under their own name; the post says that GPT-5.2 Pro appears to have determined the strategy, and the site's remarks name the system the same way.
Depends on. No page of this wiki.