Provedarithmeticdemo

Adding zero on the right

For all $\htmlData{mx=1}{n \in \htmlData{mx=0}{\mathbb{N}}}$ :

\htmlData{mx=1}{\htmlData{mx=0}{n} + 0} \mathrel{\htmlData{mx=3}{=}} \htmlData{mx=2}{n}

What the notation means · or point at any symbol

NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (Nat)
+Addition: n plus 0. (n + 0)
=Equality: n + 0 and n are the same. (n + 0 = n)

theorem add-zero-right (n : Nat) :
    n + 0 = n

For every natural number n, n + 0 = n.

How it was proved

Proved: 23 September 2026
By: Ajax, with the agent “end-to-end test agent (Claude)”
Checked by: Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
Axioms: propext
Proof: 6 lines of Lean