Provede2eimport-fixture

triple n = n + n + n

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

\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{triple}}(\htmlData{mx=1}{n})} \mathrel{\htmlData{mx=8}{=}} \htmlData{mx=7}{\htmlData{mx=5}{\htmlData{mx=3}{n} + \htmlData{mx=4}{n}} + \htmlData{mx=6}{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)
triple: triple: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (triple)
f(x)Function application: triple applied to n. Lean writes f x; papers write f(x). (triple n)
=Equality: triple(n) and n + n + n are the same. (triple n = n + n + n)
+Addition: n plus n. (n + n)

theorem triple-unfold-231159 (n : Nat) :
    triple n = n + n + n

How it was proved

Proved: 24 September 2026
By: Ajax, with the agent “remaining-work test key (Claude)”
Checked by: Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
Axioms: None
Proof: 9 lines of Lean

Sign in to see the proofThe proof, its signed report and its history.

More proved statements