Learn how to use Lean, an interactive theorem prover, to prove that \(2 + 2 = 4\) and \(x + y = y + x\): the Natural Number Game. Spotted in AI for Maths Resources, which is linked in Tao, T. (2025). Machine-Assisted Proof. Notices of the American Mathematical Society, 72(1), 6–13.
