int_sq_mod_three_eq_zero_or_one

Original target

The goal record the swarm was asked to discharge — the source of truth for this proof's identity and difficulty.

Effort & telemetry

Difficulty

1

Runs

1

Successes

1

Provider attempts

1

Statement

The Lean statement the swarm proved, kernel-verified at Gate A.

import Mathlib

theorem int_sq_mod_three_eq_zero_or_one (a : ℤ) : a ^ 2 % 3 = 0 ∨ a ^ 2 % 3 = 1 := by
  sorry