# Reach for the stars

Welcome to Stars! The object of the game is to create a certain number of stars by adding or removing stars from your current collection. You always start with a small positive number of stars. On each of your turns you can apply one of the available moves to your current collection to construct another collection (which becomes your new current collection). The list of available moves is different for each level of the game. It may require some study and investigation on your part to come up with an efficient strategy for beating this game at the higher levels of difficulty.

BONUS Challenge: Can you determine all of the possible collections you can construct from your starting collection using only the given moves?

## Game Components

As described in the Introduction, this game illustrates the basic features of a formal proof system.

• Toys: The toys in this game consist of a collection of stars. You can also view a description of each collection by pressing V.
• A Goal: The goal is a randomly selected number of stars. The object of game is to produce this many stars by applying the available moves to the collection.
• The Starting Position: The starting position in this game is always a small positive number of stars.
• The Rules: The rules you can use to add or remove stars from your collection are different in each level of the game, and are listed under the Moves menu. It is up to you to determine what the various moves do for each level by experimentation or deductive reasoning.
• Inputs: The input for both Rules consists of the current collection of stars. The current collection of stars is always shown in the last row of the table. You can undo a move and go back to a previously constructed number by pressing U.
• Output: The output is the new collection of stars produced by applying one of the Rules to the current collection. This new collection is added to the bottom of the table and becomes the current collection. If it matches the goal, you win!

## The Math Behind the Fun

This game is related to the branch of mathematics known as number theory. In particular, winning a particular game is equivalent to finding some way of expressing the difference between number of stars in the goal and the number of stars you start with as a linear combination of the given move numbers where the coefficients in the linear combination must be nonnegative integers. In some levels and instances of the game you can produce any positive number of stars. In others you cannot, in which case it is an interesting mathematical question to determine exactly which goals can be reached from the starting collection in a particular game. Fortunately, the game only picks goals which can be achieved, so you can be confident that there is a way to win the game, even if you can't find it.