TPP 2025: 21st Theorem Proving and Provers Meeting, Dec 3 Wed - 4 Thu, Tohoku University

The deadline is Nov 15 but earlier registrations are appreciated!  You can modify your registration until the deadline. https://forms.gle/jHuj7z4tBogDcBfb6 締め切りは11月15日とさせていただきますが，なるべくお早めにご登録いただければ助かります．締め切りまでは変更可能です．

解答は電子メールで tppmark2025 AT sf.ecei.tohoku.ac.jp にお送りください． E-mail your answers to: tppmark2025 AT sf.ecei.tohoku.ac.jp 追記(2025/11/18): 締め切りはTPP 2025前日12/2（火）とします．ご解答・ご解答者はTPP 2025ならびにWebにて発表いたします． The deadline is Dec 2 Tue.  Answers will be presented at TPP 2025 and on the Web. 以下の問題を定理証明支援系を用いて形式化し，証明を記述してください。 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 squar...

The 21st Theorem Proving and Provers (TPP) meeting will be held on December 3 (Wed) - 4 (Thu), 2025 at Tohoku University. 第21回Theorem Proving and Provers TPPミーティングは2025年12月3日(水)・4日(木)に東北大学で開催されます． TPP is held every year since 2005 and provides a forum to exchange ideas for both users and implementors of theorem provers and proof assistants. TPPは2005年から毎年開催され， 定理証明器や証明支援系のユーザと開発者がアイディアを交換する場を提供しています． Date: Dec 3 (Wed) afternoon - Dec 4 (Thu) exact time is to be announced later 日時: 12月3日(水)午後・4日(木) 正確な時間は後日アナウンス予定です Place: Graduate School of Information Sciences, Aobayama Campus, Tohoku University  https://www.is.tohoku.ac.jp/en/introduction/access.html 会場: 東北大学 青葉山キャンパス 情報科学研究科 2階 大講義室  https://www.is.tohoku.ac.jp/jp/introduction/access.html Online participation (via Google Meet) will be available on a best-effort basis. オンライン参加（Google Meetによる）はベストエフォートで対応する予定です． Registration / 参加登録（追記）: https://tpp2025.blogspot.com/2025/09/call-for-participation-and-presentation...