View on GitHub


The 19th Theorem Proving and Provers meeting (TPP 2023)

TPP (Theorem Proving and Provers) ミーティングは, 2005年から年に1回開催され, 定理証明系を作っている人から使う側の人まで幅広い人たちが集まり, 様々な側面からの話をしてアイディアの交換をしてきたものです.

ミーティング期間中の討論を大切にしたいと考えていますので, 出来上がった仕事の講演だけでなく,進行中の仕事,未完成の仕事についての講演も歓迎します. 参加者には可能な限りご講演いただくことを期待しています.

TPP is a series of annual meetings for developers as well as users of theorem provers. Discussions from various aspects and exchanges of ideas have taken place in the past meetings since 2005.

We regard the discussions during the meeting to be most important. As such, not only the talks about completed work, but those about ongoing work and half-baked work are also welcome. We hope all participants would consider giving a talk.

開催日程 / Date

2023年10月30日(月)-31(火) / Mon. 30th to Tue. 31st, October 2023

会場 / Venue

東京工業大学・大岡山キャンパス / Tokyo Institute of Technology, Ookayama Campus
西8号館E棟10階大会議室 / Main Conference Room, 10F, West Bldg. 8E

下記の地図の21の建物です.入り口が3階です,入り口を入って少し進んで, 左側のエレベーターで10階に進んでください.
Building 21 on the map below. The entrance is on the 3rd floor. Please enter the entrance, go a little further and take the elevator on the left to the 10th floor.

住所 / Address

〒152-8550 東京都目黒区大岡山2-12-1 / 2-12-1 Oookayama, Meguro, Tokyo 152-8550
アクセス / Access

懇親会 / Dinner Party

日時: 10月30日(月) 18:15- / Time: Oct. 30th Mon. 18:15-
会場 / Place: ビアバー SHINO - (On Google Map)
会費 / Party fee: 学生 / Student 3,000円,一般 / Other 6,000円

幹事 / Organizer

中正和久 (山口大学工学部)
Kazuhisa NAKASHO (Faculty of Engineering, Yamaguchi University)
Email: nakasho<at>

南出靖彦 (東京工業大学情報理工学院)
Yasuhiko MINAMIDE (Department of Mathematical and Computing Science, Tokyo Institute of Technology)
Email: minamide<at>

参加申し込み / Registration

10/25(水)までに / Please register by 25th October from

こちらから / here

プログラム / Technical Program

10月30日(月) / Oct. 30th (Mon.)

10月31日(火) / Oct. 31st (Tue.)


解答は中正宛(nakasho<at>にお送りください. / Please send your answer to Nakasho (nakasho<at>


N目並べは碁盤上で行うゲームで,先手と後手の二人のプレイヤーが交互に石を置いていき, 先に縦,横,斜めのいずれかの方向にN個の石を連続して直線上に並べたほうが勝ちです. 以下では,盤面は無限に大きいものとします.

  1. N目並べを形式化してください.
  2. N目並べでは後手に必勝法がないことを証明してください.
  3. Nが十分に大きければ,先手に必勝法がないことを証明してください.

In N-in-a-row game, the first and second players take turns placing stones on a Go board, and the winner being the player who first places its own N stones in a row in either vertical, horizontal, or diagonal direction. In the following, the Go board is assumed to be infinite.

  1. Formalize N-in-a-row game.
  2. Prove that there is no winning strategy for the second player in N-in-a-row game.
  3. Prove that if N is sufficiently large, the first player has no winning strategy.


Mailing List


  1. Google Groupにログインします.
  2. グループを検索します.
    • 上部の マイグループ をクリックし,すべてのグループとメッセージ を選択します.
    • 検索ボックスのグループの名前に「Theorem Proving and Provers」と入力してEnterキーを押します.
  3. 検索リストの「Theorem Proving and Provers」を選択して,グループへの参加をリクエストを押します.

The TPP Meeting manages a mailing list. You can subscribe to the mailing list by following the instructions below:

  1. log in to Google Group.
  2. search for a group.
    • At the top, click My groups and select All groups and messages.
    • In the search box, type “Theorem Proving and Provers” and press the Enter key.
  3. Select “Theorem Proving and Provers” in the search list and press Ask to join group.

これまでのTPP / Past TPPs

TPP2022 / TPP2021 / TPP2020 / TPP2019 / TPP2018 / TPP2017 / TPP2016 / TPP2015 / TPP2014 / TPP2013 / TPP2012 / TPP2011 / TPP2010 / TPP2009 / TPP2008 / TPP2007 / TPP2006 / TPP2005