minif2f-v1 / algebra-xmysqpymzsqpzmxsqeqxyz-xpypzp6dvdx3y3z3

algebra-xmysqpymzsqpzmxsqeqxyz-xpypzp6dvdx3y3z3

open

difficulty 4

credited

Run this goal:./swarm/run.sh --goal algebra-xmysqpymzsqpzmxsqeqxyz-xpypzp6dvdx3y3z3

What it runs

The Lean statement the swarm must prove — kernel-verified at Gate A. The trailing sorry is the open obligation a proof replaces.

goals/algebra-xmysqpymzsqpzmxsqeqxyz-xpypzp6dvdx3y3z3.lean

import Mathlib

set_option maxHeartbeats 0
open BigOperators Real Nat Topology Rat

theorem algebra_xmysqpymzsqpzmxsqeqxyz_xpypzp6dvdx3y3z3 (x y z : ℤ)
  (h₀ : (x - y) ^ 2 + (y - z) ^ 2 + (z - x) ^ 2 = x * y * z) :
  x + y + z + 6 ∣ x ^ 3 + y ^ 3 + z ^ 3 := by
  sorry

Runs (0)

No runs recorded for this suite yet — they appear here as the swarm attempts the benchmarks.