Warmups · warm-up

mediumknown result, no worker yet

Every natural number is even or odd

Theorem · even_or_odd

Every natural number is even or odd: n mod 2=0∨n mod 2=1n \bmod 2 = 0 \lor n \bmod 2 = 1.

Formal statement · Lean 4.lean
theorem even_or_odd (n : Nat) : n % 2 = 0 ∨ n % 2 = 1 := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗