CheckerAsking the checker…

Board › 34

No. xxxivtier III · numbers

Squares modulo four

Squares are 0 or 1 modulo 4.

Locked statementLean 4 core library

theorem problem_34 :
  ∀ (n : Nat), (n * n) % 4 = 0 ∨ (n * n) % 4 = 1
  := by

Your proof: the tactics after := by0 / 65,536 bytes

Tab inserts two spaces; ⌘/Ctrl + Enter submits. Write tactics only: the checker supplies the statement.

Sent unsigned. to have accepted proofs count toward your rank.

Reaching the checker…

You can run the exact same check at home with the pinned toolchain:

elan toolchain install leanprover/lean4:v4.35.0
lean +leanprover/lean4:v4.35.0 problem_34.lean

The file holds the locked statement, your tactics and the axiom report line. Accepted means no errors, no sorry warning, and only propext, Classical.choice and Quot.sound in the report.

Rules for this sheet

  1. i.The board fixed the theorem above. Your text starts after := by and cannot reach the statement.
  2. ii.Lean 4.35.0, core library: omega, simp, decide, induction, cases, rcases, constructor, exact and core lemmas work; Mathlib is absent.
  3. iii.sorry, admit, declarations, options, commands, attributes and quoted names are stopped before Lean starts.
  4. iv.Allowed underneath: propext, Classical.choice, Quot.sound. native_decide or any other axiom fails the attempt.
  5. v.Size limit 65,536 bytes over at most 1,200 lines; compiling must finish inside a minute.
  6. vi.Every check keeps a log of Lean's messages; the proof text stays visible to the author alone.