← The project The Lean proofs

Playground

Squares in Circles

How small can a circle be if it has to hold n unit squares that don't overlap? For n = 1 to 8, Lean proves the least radius and finds every packing that reaches it. Here you can move the squares and watch the smallest circle around them. It never gets smaller than the proved minimum.

How to play

Drag a square to move it, and drag the knob beside a selected square to turn it. Squares are solid: they stop at their neighbours and slide along them.

Keys, on the board: Enter picks a square, the arrows move it, [ and ] turn it, and Shift takes bigger steps.