Problem:

There are N children sitting in a circle, where each child has an even number of candies. The following step is repeated indefinitely: every child passes half of their candies to the child on their left; any child who ends up with an odd number of candies is given another candy by the teacher. Then, prove that eventually every child will hold the same number of candies.

Proof outline:

Let m(i,k) be the number of candies held by the i'th child (i in {1,...,N}) after k steps. At first, prove the following lemmas: (1) max(k+1) <= max(k), (2) min(k) <= min(k+1), (3) if min(k) < m(i,k) then min(k) < m(i,k+1), (4) if m(i,k) < m(right(i),k) then m(i,k) < m(i,k+1), where max(k) = max{m(i,k) | i in {1,...,N}}, min(k) = min{m(i,k) | i in {1,...,N}}, right(i) = (if (i < N) then (i+1) else 1). Then, prove the following lemma: (5) if (min(k) < m(i,k)) for some i, then num(min(k),k+1) < num(min(k),k), where num(m,k) is the number of children holding m candies after k steps. Finally, it can be proven that all the children eventually hold the same number of candies.

Reference:

- Bohman, T., Pikhurko, O., Frieze, A., Sleator, D.:

The Puzzle TOAD, Puzzle 6: Uniform Candy Distribution.

Carnegie Mellon, School of Computer Science. Solution. Last access: 2011/10/13.

Solutions using theorem provers:

- Isabelle 磯部 祥尚 (Yoshinao Isobe) (slides) (script)
- Coq 山本 光晴 (Mitsuharu Yamamoto) (script)
- Coq 才川隆文 (Takafumi Saikawa) (script)
- SSReflect Reynald Affeldt (アフェルト レナルド) (pdf) (script)
- Z3 酒井 政裕 (Masahiro Sakai) (script UTF-8 encoding) (local copy)
- Coq Jacques Garrigue (雅利賀 惹玖) script
- Isabelle 南出 靖彦 (Yasuhiko Minamide) script