SuperBEST Game

Six levels. Each shows a target expression and four candidate routings — pick the cheapest correct one. The right answer comes with the Lean theorem or witness that proves it.

Level 1 / 6Score 0 / 0
Target

Multiplication on positives

x · y (x, y > 0)