NIM paper · interactive edition Interactive edition · paper, explanations and Lean proofs.

Section 6.2, paragraph 1A noisy teacher plays optimally with probability 1−ε and otherwise uniformly at random

Informal interpretation Motivation, interpretation or scope; not a formal claim.

1 Paper text

Let πopt\pi_{\mathrm{opt}} denote an optimal NIM policy (move to nim-sum 00 whenever possible). For a noise parameter ε∈[0,1]\varepsilon\in[0,1], define a noisy teacher πTε\pi_T^{\varepsilon} that plays according to πopt\pi_{\mathrm{opt}} with probability 1−ε1-\varepsilon and otherwise chooses a uniformly random legal move. Occasional random moves broaden state coverage and, crucially for two-frame agents, generate diverse transition pairs (Q,Q′)(Q,Q') from which the local difference signal Δ(Q,Q′)\Delta(Q,Q') can be inferred.

Generated from paper_jmlr.tex, lines 917–919.

2 Explain this

The noisy teacher plays the optimal move (to nim-sum zero) with probability 1−ε1-\varepsilon and otherwise a uniformly random legal move. Random moves broaden the positions seen and, for two-frame agents, create varied transition pairs from which the difference signal can be learned.

Note: the dataset actually reported in Section 7.2 is generated by a specific teacher–random–teacher scheme (optimal move, then one uniformly random move, then the optimal labels), not by sampling games from πTε\pi_T^\varepsilon with a stated ε\varepsilon.

3 How this is formalised

A definition used to describe data generation. It is not formalised and no theorem depends on it.

Coverage record
Paper anchorsec:teacher-p1 (website anchor; the manuscript has no label here)
Displayed asSection 6.2, paragraph 1
ClaimA noisy teacher plays optimally with probability 1−ε and otherwise uniformly at random
Coverage categoryInformal interpretation
Statement sourcepaper_jmlr.tex lines 917–919; SHA-256 of the normalised block source 1ab56c68163ed398…
Explanationsexplain/c-noisy-teacher, formal/c-noisy-teacher
Build evidencefresh isolated rebuild, audit report

4 Lean statement and source

No Lean statement corresponds to this claim. This is interpretation or motivation, not a formal mathematical claim.

Build evidence: fresh isolated rebuild of all 38 bundled modules with Lean (version 4.26.0, started 2026-10-10T15:21:56Z, finished 2026-10-10T15:27:00Z: 38/38 modules compiled, 1588 axiom reports, no errors. See Build for the commands and the independent audit of 2026-10-10 (dated evidence).