three_dvd_all_of_sq_add_sq_eq_three_mul_sq

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

3

Statement

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

import Mathlib

theorem three_dvd_all_of_sq_add_sq_eq_three_mul_sq (x y z : ℤ) (h : x ^ 2 + y ^ 2 = 3 * z ^ 2) : 3 ∣ x ∧ 3 ∣ y ∧ 3 ∣ z := by
  sorry