minif2f-v1 / amc12a-2008-p15

amc12a-2008-p15

proved

difficulty 4

credited

Run this goal:./swarm/run.sh --goal amc12a-2008-p15

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/amc12a-2008-p15.lean

import Mathlib

set_option maxHeartbeats 0
open BigOperators Real Nat Topology Rat

theorem amc12a_2008_p15 (k : ℕ) (h₀ : k = 2008 ^ 2 + 2 ^ 2008) : (k ^ 2 + 2 ^ k) % 10 = 6 := by
  sorry

Runs (1)

Goal	Contributor	Model	Date (UTC)	Time	Result	Verification
amc12a-2008-p15	cgbarlow	claude/fable	2026-07-29 06:48	36m 19s	pass	kernel