Trying out Lean

I read an article in Skrolli magazine about how Large language models are solving math problems using programming language Lean. This got me interested to try Lean myself which led me to Natural Number Game - a gamified tutorial for Lean.

In the game the first “world” had proving 2 + 2 = 4 in Lean as final boss. The first world starts with just following “tactics”

• rfl proves goals of the form X = X
• rw a way to “substitute in”

Numbers in Lean are defined by two rules.

• 0 is a number.
• If n is a number, then the successor succ n of n is a number.

From these building blocks the goal was to prove 2 + 2 = 4.

Below is my solution

import Mathlib.Tactic

open Nat

-- these were build during the first world
theorem two_eq_succ_one : (2 : ℕ) = succ 1 := rfl
theorem three_eq_succ_two : (3 : ℕ) = succ 2 := rfl
theorem four_eq_succ_three : (4 : ℕ) = succ 3 := rfl
theorem succ_eq_add_one (n : ℕ) : n + 1 = succ n  := rfl
-- add_succ : n + succ m = succ (n + m) — already in core Lean/Mathlib as Nat.add_succ

example : (2 : ℕ) + 2 = 4 := by
  nth_rewrite 2 [two_eq_succ_one]
  rw [add_succ]
  rw [← succ_eq_add_one] -- In actual Lean 4 rw tries rfl automatically and already succeeds here
  rw [← three_eq_succ_two]
  rw [← four_eq_succ_three]
  rfl