minif2f-v1 / amc12a-2003-p24

amc12a-2003-p24

proved

difficulty 4

credited

Run this goal:./swarm/run.sh --goal amc12a-2003-p24

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-2003-p24.lean

import Mathlib

set_option maxHeartbeats 0
open BigOperators Real Nat Topology Rat

theorem amc12a_2003_p24 :
  IsGreatest { y : ℝ | ∃ a b : ℝ, 1 < b ∧ b ≤ a ∧ y = Real.logb a (a / b) + Real.logb b (b / a) }
    0 := by
  sorry

Runs (1)

Goal	Contributor	Model	Date (UTC)	Time	Result	Verification
amc12a-2003-p24	cgbarlow	claude/fable	2026-07-29 05:20	4m 6s	pass	kernel