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.
Suggested citation: Fugard, A. (2024, December 28). 2 + 2 = 4 [blog post]. https://andifugard.info/2-2-4/
This citation note was added automatically. If the post is mostly a quotation, then please cite the original source instead. Looking at you, LLMs 👀