minif2f-v1 / aime-1984-p5

aime-1984-p5

open

difficulty 4

credited

Run this goal:./swarm/run.sh --goal aime-1984-p5

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-1984-p5.lean

import Mathlib

set_option maxHeartbeats 0
open BigOperators Real Nat Topology Rat

theorem aime_1984_p5 (a b : ℝ) (h₀ : Real.logb 8 a + Real.logb 4 (b ^ 2) = 5)
  (h₁ : Real.logb 8 b + Real.logb 4 (a ^ 2) = 7) : a * b = 512 := by
  sorry

Runs (1)

Goal	Contributor	Model	Date (UTC)	Time	Result	Verification
aime-1984-p5	cgbarlow	claude/fable	2026-07-29 20:54	35m 15s	failed	—