Formal Computer Science / Computation

Kenton Labs / Computation

Game theory

A winning move is defined against optimal opponent responses, rather than against one friendly execution.

The vocabulary.

These definitions state the objects and properties used by the dataset. The complete instance specification remains the authority for each result.

Normal play
The player with no legal move loses.
Winning position
A state with at least one move to a losing position for the opponent.
Strategy
A legal choice for every winning state in the declared game domain.

How the dataset works.

Three deterministic instances define this family. Each includes its input model, a checked result, evidence, and an acceptance procedure. Download the complete dataset JSON ↘ or the area’s readable source ↘.

Acceptance procedure

  1. Set the empty heap to losing.
  2. Process heap sizes in increasing order.
  3. Mark a heap winning if an allowed subtraction reaches a losing heap.
  4. Validate every submitted winning move and every losing-state marker.

Cost and scope

N heap sizes with m allowed moves require O(Nm) dynamic-programming checks.

A common failure

A single successful play does not establish a strategy against all opponent choices.

Worked records.

Three instances expose concrete claims and the artifacts that establish or refute them. Expand a record for the problem, checker reasoning, formal payload, and verification metadata.

KL-FCS-049
Game theoryTake one or two stonesComplete backward classification · 13 states

The problem

Classify each heap size and certify a winning strategy under optimal normal play.

The checked result

Winning heap sizes: [1, 2, 4, 5, 7, 8, 10, 11].

Every winning state has a legal move to a losing state. A losing state has no such move, so the opponent controls the next winning position.

Why the checker accepts it

  1. Set the empty heap to losing.
  2. Process heap sizes in increasing order.
  3. Mark a heap winning if an allowed subtraction reaches a losing heap.
  4. Validate every submitted winning move and every losing-state marker.

Formal specification

{
  "moves": [
    1,
    2
  ],
  "max_heap": 12,
  "terminal_rule": "A player unable to move loses; no draws; perfect information."
}

Claim and evidence

{
  "claim": {
    "winning_positions": [
      1,
      2,
      4,
      5,
      7,
      8,
      10,
      11
    ]
  },
  "witness": {
    "strategy": [
      null,
      1,
      2,
      null,
      1,
      2,
      null,
      1,
      2,
      null,
      1,
      2,
      null
    ]
  }
}

Dataset construction

Deterministic finite fixture; full enumeration or witness replay as stated. Structured JSON; field meanings are stated in the specification. Acceptance covers 13 checker units for this record; the unit type is stated in its verification scope.

Complexity and limits

N heap sizes with m allowed moves require O(Nm) dynamic-programming checks.

These are finite impartial subtraction games, not equilibrium analyses of simultaneous or imperfect-information games.

A boundary to investigate

A single successful play does not establish a strategy against all opponent choices. Add alternating-player reachability graphs and strategy certificates.

Verification and provenance metadata

Mechanical status: checked. Human review: not yet recorded. Checker version 1.0.0, Python 3.9.6. The report contains source hashes. The trust boundary includes Python and the custom checker implementations; no proof-assistant validation is claimed.

Original Kenton Labs reference instance, authored with Codex assistance on 2026-10-11. No external dataset import or model-generation evaluation. Reuse-license selection remains pending.

Replay from the source bundle: python3 tools/verify.py.

Readable source ↘Record JSON ↘Full area ↗Related KL-FCS-050 ↘Related KL-FCS-051 ↘
KL-FCS-050
Game theoryOdd-sized subtraction choicesComplete backward classification · 17 states

The problem

Classify each heap size and certify a winning strategy under optimal normal play.

The checked result

Winning heap sizes: [1, 3, 5, 7, 9, 11, 13, 15].

Every winning state has a legal move to a losing state. A losing state has no such move, so the opponent controls the next winning position.

Why the checker accepts it

  1. Set the empty heap to losing.
  2. Process heap sizes in increasing order.
  3. Mark a heap winning if an allowed subtraction reaches a losing heap.
  4. Validate every submitted winning move and every losing-state marker.

Formal specification

{
  "moves": [
    1,
    3
  ],
  "max_heap": 16,
  "terminal_rule": "A player unable to move loses; no draws; perfect information."
}

Claim and evidence

{
  "claim": {
    "winning_positions": [
      1,
      3,
      5,
      7,
      9,
      11,
      13,
      15
    ]
  },
  "witness": {
    "strategy": [
      null,
      1,
      null,
      1,
      null,
      1,
      null,
      1,
      null,
      1,
      null,
      1,
      null,
      1,
      null,
      1,
      null
    ]
  }
}

Dataset construction

Deterministic finite fixture; full enumeration or witness replay as stated. Structured JSON; field meanings are stated in the specification. Acceptance covers 17 checker units for this record; the unit type is stated in its verification scope.

Complexity and limits

N heap sizes with m allowed moves require O(Nm) dynamic-programming checks.

These are finite impartial subtraction games, not equilibrium analyses of simultaneous or imperfect-information games.

A boundary to investigate

A single successful play does not establish a strategy against all opponent choices. Add alternating-player reachability graphs and strategy certificates.

Verification and provenance metadata

Mechanical status: checked. Human review: not yet recorded. Checker version 1.0.0, Python 3.9.6. The report contains source hashes. The trust boundary includes Python and the custom checker implementations; no proof-assistant validation is claimed.

Original Kenton Labs reference instance, authored with Codex assistance on 2026-10-11. No external dataset import or model-generation evaluation. Reuse-license selection remains pending.

Replay from the source bundle: python3 tools/verify.py.

Readable source ↘Record JSON ↘Full area ↗Related KL-FCS-049 ↘Related KL-FCS-051 ↘
KL-FCS-051
Game theoryA game with a nontrivial move setComplete backward classification · 21 states

The problem

Classify each heap size and certify a winning strategy under optimal normal play.

The checked result

Winning heap sizes: [2, 3, 4, 5, 6, 9, 10, 11, 12, 13, 16, 17, 18, 19, 20].

Every winning state has a legal move to a losing state. A losing state has no such move, so the opponent controls the next winning position.

Why the checker accepts it

  1. Set the empty heap to losing.
  2. Process heap sizes in increasing order.
  3. Mark a heap winning if an allowed subtraction reaches a losing heap.
  4. Validate every submitted winning move and every losing-state marker.

Formal specification

{
  "moves": [
    2,
    3,
    5
  ],
  "max_heap": 20,
  "terminal_rule": "A player unable to move loses; no draws; perfect information."
}

Claim and evidence

{
  "claim": {
    "winning_positions": [
      2,
      3,
      4,
      5,
      6,
      9,
      10,
      11,
      12,
      13,
      16,
      17,
      18,
      19,
      20
    ]
  },
  "witness": {
    "strategy": [
      null,
      null,
      2,
      2,
      3,
      5,
      5,
      null,
      null,
      2,
      2,
      3,
      5,
      5,
      null,
      null,
      2,
      2,
      3,
      5,
      5
    ]
  }
}

Dataset construction

Deterministic finite fixture; full enumeration or witness replay as stated. Structured JSON; field meanings are stated in the specification. Acceptance covers 21 checker units for this record; the unit type is stated in its verification scope.

Complexity and limits

N heap sizes with m allowed moves require O(Nm) dynamic-programming checks.

These are finite impartial subtraction games, not equilibrium analyses of simultaneous or imperfect-information games.

A boundary to investigate

A single successful play does not establish a strategy against all opponent choices. Add alternating-player reachability graphs and strategy certificates.

Verification and provenance metadata

Mechanical status: checked. Human review: not yet recorded. Checker version 1.0.0, Python 3.9.6. The report contains source hashes. The trust boundary includes Python and the custom checker implementations; no proof-assistant validation is claimed.

Original Kenton Labs reference instance, authored with Codex assistance on 2026-10-11. No external dataset import or model-generation evaluation. Reuse-license selection remains pending.

Replay from the source bundle: python3 tools/verify.py.

Readable source ↘Record JSON ↘Full area ↗Related KL-FCS-049 ↘Related KL-FCS-050 ↘

Go further.

Add alternating-player reachability graphs and strategy certificates.

Questions to investigate

  1. A single successful play does not establish a strategy against all opponent choices.
  2. Which assumption in the specification can be changed to make the current evidence insufficient?
  3. Add alternating-player reachability graphs and strategy certificates.

Conceptual references

These sources explain the surrounding theory. The linked material was not imported as a dataset, and these records do not claim checking by the source’s software.

Primary conceptual reference ↗

Related areas

AlgorithmsGraph algorithmsRelational algebra