View on GitHub


The 16th Theorem Proving and Provers meeting (TPP 2020)

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

2020年11月16日(月) / Mon. 16th, November.

会場 / Venue

今年度はコロナウイルス感染症 (COVID-19)の感染拡大防止のため,オンライン(Zoom)で開催する予定です. 事前に参加申し込みしていただいた方々には別途,接続方法等の詳細をお知らせします.

In order to prevent the spread of coronavirus infection (COVID-19), we are planning to hold an online meeting (Zoom) this year. Those who have registered in advance will be notified of the details of how to join the meeting.

懇親会 / Dinner Party

幹事 / Organizer

中正和久 (山口大学工学部) / Kazuhisa NAKASHO (Faculty of Engineering, Yamaguchi University)

Email: nakasho<at>

参加申し込み / Registration

11/11(水)までに / Please register by 11th November from

こちらから / here

プログラム / Technical Program

Nov. 16


modified at 20:30, Sep. 28th, 2020

SAT/SMTソルバで解を探索するような問題にしてみました.それぞれ手証明も可能です.回答は nakasho まで送付をお願いします.

I made problems to find the solutions using SAT/SMT solvers. You can also prove them without solvers. Please send your answer to nakasho


124本のベクトルからなる集合 X = {(x,y,z) | x,y,z ∈ {0,±1,±√2}} \ {(0,0,0)} の各要素を白または黒に塗り分けることを考えます. このとき,次の2条件 a), b) を満たすようにベクトルを白または黒に塗り分けることはできないことを証明してください.

Consider painting each element of the set X = {(x,y,z) | x,y,z ∈ {0,±1,±√2}} \ {(0,0,0)} of 124 vectors white or black. Prove that the vectors cannot be painted white or black in such a way that the following two conditions a) and b) are met.


条件 c) を満たしつつ,条件 a) と b) の少なくとも一方は成り立たないように,ベクトルの集合 X からできるだけ多くの要素を減らしてください. (ヒント: 33本までは減らせることが知られています.)

Reduce as many elements as possible from the set of vectors X such that at least one of the conditions a) and b) does not hold while condition c) is satisfied. (Hint: It is known that you can reduce the number to 33.)


より一般的に n 次元 (n > 3) の場合に拡張してください. このとき問題は,条件 c’) を満たしつつ,条件 a) と b’) の少なくとも一方は成り立たないように, n 次元ベクトルの集合を見つけることとなります.

一般の場合はとても難しいです.特定の n (> 3) に対して,このようなベクトルの集合を構成する回答も歓迎します.

More generally, extend it to the case of n dimensions (n > 3). The problem is to find a set of n-dimensional vectors such that at least one of the conditions a) and b’) does not hold while condition c’) is satisfied.

The general case is very difficult. The constitution of such a set of vectors for a particular n (> 3) is also welcome.

解答 / Solutions

これまでのTPP / Past TPPs

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