minif2f-v1 / algebra-3rootspoly-amdtamctambeqnasqmbpctapcbtdpasqmbpctapcbta

algebra-3rootspoly-amdtamctambeqnasqmbpctapcbtdpasqmbpctapcbta

open

difficulty 4

credited

Run this goal:./swarm/run.sh --goal algebra-3rootspoly-amdtamctambeqnasqmbpctapcbtdpasqmbpctapcbta

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-3rootspoly-amdtamctambeqnasqmbpctapcbtdpasqmbpctapcbta.lean

import Mathlib

set_option maxHeartbeats 0
open BigOperators Real Nat Topology Rat

theorem algebra_3rootspoly_amdtamctambeqnasqmbpctapcbtdpasqmbpctapcbta (b c d a : ℂ) :
    (a - d) * (a - c) * (a - b) =
      -((a ^ 2 - (b + c) * a + c * b) * d) + (a ^ 2 - (b + c) * a + c * b) * a := by
  sorry

Runs (0)

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