Wiki
Wiki

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 (2348+o(1))n(\tfrac{23}{48}+o(1))n moves. For any ϵ<1/24\epsilon<1/24 the game therefore cannot be guaranteed to last (1−ϵ)n2(1-\epsilon)\tfrac{n}{2} moves for all large nn, 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 CC of odd numbers, and improves the saving from 1/241/24 to 1/151/15 by taking CC to be the odd numbers in (n/5,n/3](n/5,n/3], and in an edit to 8/1058/105 by taking the odd numbers in (n/7,n/3](n/7,n/3] not divisible by 55: the multiples 2s2s, 3s3s and 4s4s of elements of CC 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 (1−ε)n2(1-\varepsilon)\frac{n}{2} 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 (1−ϵ)n2(1-\epsilon)\tfrac{n}{2} moves, answered in the negative when Prolonger moves first. It does not cover the first displayed question, the ϵn\epsilon n threshold, nor the order of the guaranteed length L(n)L(n), 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 L(n)=o(n)L(n)=o(n), 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 (2348+o(1))n(\tfrac{23}{48}+o(1))n 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 23/4823/48 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.