minif2f-v1 / aime-1990-p2

aime-1990-p2

proved

difficulty 4

credited

Run this goal:./swarm/run.sh --goal aime-1990-p2

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/aime-1990-p2.lean

import Mathlib

set_option maxHeartbeats 0
open BigOperators Real Nat Topology Rat

theorem aime_1990_p2 :
  (52 + 6 * Real.sqrt 43) ^ ((3 : ℝ) / 2) - (52 - 6 * Real.sqrt 43) ^ ((3 : ℝ) / 2) = 828 := by
  sorry

Runs (1)

Goal	Contributor	Model	Date (UTC)	Time	Result	Verification
aime-1990-p2	cgbarlow	claude/fable	2026-07-29 21:11	4m 25s	pass	kernel