Scales

A classic puzzle involves determining the minimum number of times a scale must be used to find a single fake coin in a collection of coins. This project concerns using formal methods to prove properties regarding such puzzles. In particular, we prove that the algorithm given for finding a fake coin known to be lighter than the real coins is optimal for any number of coins.

This proof is formalized in Coq.

Enjoy,

Fred Smith