解答は電子メールで 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 3 個並べて，全体として n × n × n の大きな立方体を作る． すると，その外面には各面に n × n 個，計 6 n 2 個の小正方形（外側に見えているランプの外面）が現れる． 各ランプは on/off のいずれかの状態をもち，外面の小正方形のうち一つを押すと，その小正方形とちょうど反対側にある小正方形を結ぶ直線上(*1)の n 個のランプだけが同時に反転（on↔off）する． 全ランプの on/off の状態が与えられたとき，上記の操作の繰り返しのみですべてのランプを off にできるための必要十分条件をなるべく簡潔に記述し，その条件の正しさを証明せよ． (*1) 追記(2025/9/16):「その小正方形とちょうど反対側にある小正方形を結ぶ直線上」は「その小正方形を垂直に貫通する直線上」の意です． Problem Let n ≥1 be an integer. Arrange n 3 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 6 n 2 squares. Each lamp is either on or off. When one of the small squares on ...