TPPmark 2025

解答は電子メールで tppmark2025 AT sf.ecei.tohoku.ac.jp にお送りください．
E-mail your answers to: tppmark2025 AT sf.ecei.tohoku.ac.jp

以下の問題を定理証明支援系を用いて形式化し，証明を記述してください。
Formalize the following problem and give your proof on a proof assistant.

問題

n ≥1 を整数とする．同じサイズの立方体型ランプを隙間なく n³ 個並べて，全体として n×n×n の大きな立方体を作る． すると，その外面には各面に n×n 個，計 6n² 個の小正方形（外側に見えているランプの外面）が現れる． 各ランプは on/off のいずれかの状態をもち，外面の小正方形のうち一つを押すと，その小正方形とちょうど反対側にある小正方形を結ぶ直線上(*1)の n 個のランプだけが同時に反転（on↔off）する．

全ランプの on/off の状態が与えられたとき，上記の操作の繰り返しのみですべてのランプを off にできるための必要十分条件をなるべく簡潔に記述し，その条件の正しさを証明せよ．

(*1) 追記(2025/9/16):「その小正方形とちょうど反対側にある小正方形を結ぶ直線上」は「その小正方形を垂直に貫通する直線上」の意です．

Problem

Let n ≥1 be an integer. Arrange n³ identical cube-shaped lamps tightly, forming a large n×n×n cube. On each outer face, an n×n grid of small squares (the exposed faces of the lamps on that face) is visible, for a total of 6n² squares. Each lamp is either on or off. When one of the small squares on the outer surface is pressed, the n lamps on the straight line joining the pressed square and the square directly opposite it on the far face (*1) toggle simultaneously (on↔off).

Given the on/off configuration of all lamps, describe as concisely as possible a necessary and sufficient condition on the configuration to be turned off by repeated applications of the above operation, and prove the correctness of the condition.

(*1) Clarification (Sep 16, 2025): "on the straight line joining the pressed square and the square directly opposite it on the far face" means "on a straight line which vertically penetrates the pressed square".

作題: 中野 圭介
Credit: Keisuke Nakano