References Mathematics in Lean by Jeremy Avigad and Patrick Massot Mathlib 4 API docs Lean Zulip Chat Some Lean Games The original version of The Natural Number Game