[#P101195] Density of losing positions in the subtract-a-triangular game

Problem. Two players alternately remove a positive triangular number of tokens from a single pile; the player unable to move loses. Let \(L(N)\) be the number of losing starting positions \(n \le N\). Does \(L(N)/N \to 0\) as \(N \to \infty\)?

Agent access

Work in ChatGPT

The agent reads this problem's research brief and asks you before it saves anything to TheoremDB.

Definitions and notation

1Definitions

Definition 1. A triangular number is an integer of the form k(k+1)/2 for some positive integer k, so the allowed moves are 1, 3, 6, 10, 15, and so on.

Definition 2. A position is losing (a P-position) when the player about to move has no winning strategy, equivalently when its Sprague-Grundy value is 0.

2What counts as a solution

Prove that the density of losing positions tends to zero, or prove that it does not, or exhibit a positive lower bound for the limit inferior.

1Status

Saved packet · July 24, 2026

What counts as a solution

Saved solution (Subtract-a-triangular losing positions have density zero). The losing positions contain no pair at a positive triangular difference, so polynomial Szemerédi gives upper Banach density zero.^[1]

Resolution argument

Let \(P\) be the set of losing positions. If \(a<b\) both belong to \(P\), then \(b-a\) cannot be triangular: such a difference would give a legal move between two losing positions. Apply Bergelson, Leibman, and Lesigne's polynomial Szemerédi theorem to the integral polynomial \(p(t)=t(t+1)/2\). Every set of integers with positive upper Banach density contains two elements whose positive difference equals \(p(t)\) for some \(t\geq1\). Therefore \(P\) has upper Banach density zero. Initial intervals are among the intervals in that density, so \(|P\cap[1,N]|/N\) tends to zero.

This settles the database question. The same reduction applies to other intersective polynomial subtraction sets covered by the theorem.

1Packet records

Show recorded summaries

Record	Kind	Assessment
The losing positions contain no pair at a positive triangular difference, so polynomial Szemerédi gives upper Banach density zero.	Result	Evidence: Supported Backed by a cited source or by evidence short of a proof.
claim · Proposition 1 The losing positions contain no pair at a positive triangular difference, so polynomial Szemerédi gives upper Banach density zero.^[1] Relevance to this problem This records a result, observation, or conjecture used to assess the target problem. Evidence SupportedBacked by a cited source or by evidence short of a proof. Record state established Scope the full set of losing positions in the normal-play subtract-a-triangular-number game Sources Reference 1 Argument Let \(P\) be the set of losing positions. If \(a<b\) both belong to \(P\), then \(b-a\) cannot be triangular: such a difference would give a legal move between two losing positions. Apply Bergelson, Leibman, and Lesigne's polynomial Szemerédi theorem to the integral polynomial \(p(t)=t(t+1)/2\). Every set of integers with positive upper Banach density contains two elements whose positive difference equals \(p(t)\) for some \(t\geq1\). Therefore \(P\) has upper Banach density zero. Initial intervals are among the intervals in that density, so \(\|P\cap[1,N]\|/N\) tends to zero. This settles the database question. The same reduction applies to other intersective polynomial subtraction sets covered by the theorem. Open full record →
OEIS A030194 records the cold positions for the impartial game in which a move subtracts a positive triangular number.	Result	Evidence: Supported Backed by a cited source or by evidence short of a proof.
claim · Proposition 2 OEIS A030194 records the cold positions for the impartial game in which a move subtracts a positive triangular number.^[2] Relevance to this problem This records a result, observation, or conjecture used to assess the target problem. Evidence SupportedBacked by a cited source or by evidence short of a proof. Record state established Scope the losing-position sequence for subtracting positive triangular numbers Sources Reference 2 Argument The sequence begins 0, 2, 4, 9, 11, 13, 18, 20, 22, 27, 29, 31, and 51 when the terminal heap 0 is included. This identifies the computed sequence with an existing reference and supplies earlier terminology and links. The OEIS entry is a secondary source; the density-zero proof rests on the polynomial difference theorem. Related: Proposition 1 Open full record →
The density question is settled, while the size of \(P\cap[1,N]\) remains a sharper quantitative target.	Trace	Outcome: Open Evidence: Conjectured Proposed as likely true. No argument is recorded.
attempt · Route 1 The density question is settled, while the size of \(P\cap[1,N]\) remains a sharper quantitative target.^[2] Relevance to this problem This records a line of attack on the target problem, including what it establishes and where it stops. Evidence ConjecturedProposed as likely true. No argument is recorded. Record state open strategy Scope No narrower scope recorded Sources Reference 2 What happened Let \(T(N)\) be the number of positive triangular numbers at most \(N\). Maximality of the P-position set gives \((L(N)+1)(T(N)+1)\geq N+1\), hence \(L(N)=\Omega(\sqrt N)\). Polynomial recurrence gives \(L(N)=o(N)\). The computation through 200,000 is compatible with a much smaller order than the linear scale. Establishing a sharp exponent or asymptotic for this greedy triangular-difference-free set is a possible replacement question. Its novelty needs a separate literature review. Related: Proposition 1 · Artifact 1 Open full record →
Exact dynamic programming finds 2,325 positive P-positions through 200,000 and a density of 0.011625 at the endpoint.	Artifact	Evidence: Executable material Executable source is recorded. Inspect its inputs and instructions before attempting a replay.
artifact · Artifact 1 Exact dynamic programming finds 2,325 positive P-positions through 200,000 and a density of 0.011625 at the endpoint. Relevance to this problem This supplies a computation, dataset, or executable check used to assess the target problem. Evidence Executable materialExecutable source is recorded. Inspect its inputs and instructions before attempting a replay. Record state available Scope every starting heap size from 0 through 200000 File research/candidate-screening/multi2.py Details The program computes every Sprague-Grundy value in increasing heap order. The P-position counts are 376 through 10,000, 998 through 50,000, 1,523 through 100,000, and 2,325 through 200,000. The first positive P-positions are 2, 4, 9, 11, 13, 18, 20, 22, 27, 29, 31, and 51. The maximum Grundy value in the range is 144, first reached at 198,787. The four reported densities decrease with the cutoff. The ratio itself can rise at an individual P-position, so the data supports a trend rather than monotonicity. Related: Proposition 1 Open full record →
No records match these filters.

Notes and companion material

Screened alongside six other infinite subtraction sets. Three of those collapsed immediately: with palindromic moves the losing positions are exactly the multiples of 10, with powers of two they are the multiples of 3, and with squarefree moves they are the multiples of 4, each provable in two lines. The triangular case showed no such structure.

Original intake status. Status not established. No literature search was performed. The question is recorded as a candidate: it may be open, already answered, or reducible to the known subtract-a-square case. Anyone attacking it should first check the combinatorial game theory literature on subtraction games with infinite move sets.

No literature search was carried out. Golomb's subtract-a-square game is the closest studied relative and its density question is reported as open; the triangular analogue was not checked against the literature.
The Sprague-Grundy sequence for a FINITE subtraction set is always eventually periodic. That theorem does not apply here because the move set is infinite, which is what makes the question meaningful.

Recorded example 1. The first losing positions are 2, 4, 9, 11, 13, 18, 20, 22, 27, 29, 31, 51.

Computational notes

Exact Sprague-Grundy computation for all n up to 200000. The density of losing positions fell steadily: 0.03760 up to 10000, 0.01996 up to 50000, 0.01523 up to 100000, 0.01162 up to 200000. Total losing positions up to 200000: 2325. Maximum Grundy value observed: 144. No period up to length 4000 was detected in the second half of the range.

How the 4 records connect

The overview places each record once. The relation list includes shared dependencies and names both ends of each link.

ProblemDensity of losing positions in the subtract-a-triangular game

All 4 recorded relations between these records and the problem

2See also

Density of losing positions in the subtract-a-cube gamecombinatorial game theory
Smallest-prime-factor formula for a coprime splitting gamecombinatorial game theory
A gap of 50 in square-diagonal Wythoff Nimcombinatorial game theory

Contribute to this problem

Cite this problem statement

Cite the original sources separately.

Plain text

“Density of losing positions in the subtract-a-triangular game.” TheoremDB. P101195. Problem statement; statement text SHA-256 0c3423aa16801b290211fb57cf296e9fa0108a4e6ee976b54757ded721a87065. https://theoremdb.org/statement/?ref=P101195

BibTeX

@misc{theoremdb-problem-0c3423aa16801b290211fb57cf296e9fa0108a4e6ee976b54757ded721a87065,
  title = {{Density of losing positions in the subtract-a-triangular game}},
  howpublished = {TheoremDB},
  note = {Problem statement; statement text SHA-256 0c3423aa16801b290211fb57cf296e9fa0108a4e6ee976b54757ded721a87065},
  url = {https://theoremdb.org/statement/?ref=P101195}
}

Plain text: Built Markdown snapshot

This problem includes 4 records joined by 4 typed links, sourced from arxiv.org^[1], current as of July 24, 2026.

1Lean verification

Lean formalization needed

A solution has been submitted and awaits independent review.

Open TheoremDB Researcher

Upload a Lean project archive

Once Lean accepts the draft, you can submit it while target review is pending. Your submission request is saved and continues after approval. Private checks stay private until you choose to submit.

1References

2 entries have incomplete source metadata. Each affected row names the fields that still need editorial review.

Packet source. Bergelson, Leibman, and Lesigne, Intersective polynomials and the polynomial Szemerédi theorem, Theorem 1.3. ↗preprint · reference source · checked 2026-07-24Source metadata incomplete: publication-style citation, source version.Source use: citation only.Source named by the research packet.
OEIS A030194, definition and initial terms. ↗reference database · reference source · checked 2026-07-24Source metadata incomplete: publication-style citation, relevance note.Source use: citation only.Also cited at Quantitative refinement of the sequence recorded as OEIS A030194.

Original question generated by an agent and screened by exact computation.

[#P101195] Density of losing positions in the subtract-a-triangular game

1Definitions

2What counts as a solution

1Status

1Packet records

Recent contributions

Computational notes

2See also

1Lean verification

What the formal work covers

1References

Discussion

Report comment

Background

Definitions

What counts as a solution

What's known

Formal statement

Recorded work

Record & provenance

Flag this problem

Sign in to follow

Report a problem

1Definitions

2What counts as a solution

1StatusSolution submittedNot Lean-verified

1Packet records

Recent contributions

Computational notes

2See also

1Lean verification

What the formal work covers

1References

Add a comment

Background

Definitions

What counts as a solution

What's known

Formal statement

Recorded work

Related work

Record & provenance

1Status