Inequalities · hard

Statement, exactly as the model and Lean see it

theorem lg_target (a b c : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a / b + b / c + c / a ≥ 3 := by

Source: Written for LeanGraph, reference proof certified
Premises used by the reference proof: 87

Traces

Each configuration's full record: what was retrieved, what the model wrote, what Lean said back.

Not verified1 model calls · 1 Lean checks · $0.00015

Attempts

sample 0 · round 0Lean 3 syntax9.2 s model time

Proof

have h1 : (a / b + b / c + c / a) ≥ 3 :=
  let a_pos := ha
  let b_pos := hb
  let c_pos := hc
  let a_b := a / b
  let b_c := b / c
  let c_a := c / a
  let sum := a_b + b_c + c_a
  let prod := (a_b * b_c * c_a)
  have h2 : prod = 1 :=
    by simp [a_b, b_c, c_a, mul_assoc, mul_left_comm, mul_one]
  let h3 : (a_b + b_c + c_a) ≥ 3 :=
    by apply (real.mul_self_le_of_ge_one (a_b * b_c * c_a) 3)
    by apply (real.ge_three_of_ge_one_and_ge_one_and_ge_one a_b b_c c_a)
    by apply (real.ge_one_of_pos a_b)
    by apply (real.ge_one_of_pos b_c)
    by apply (real.ge_one_of_pos c_a)
  exact h3
exact h1

What Lean printed (this is all the model sees on repair)

14:9: error: `simp` made no progress
16:16: error: Unknown identifier `real.mul_self_le_of_ge_one`
17:16: error: Unknown identifier `real.ge_three_of_ge_one_and_ge_one_and_ge_one`
3:100: error: unsolved goals
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
h1 : a / b + b / c + c / a ≥ 3
⊢ a / b + b / c + c / a ≥ 3
18:6: error: unexpected token 'by'; expected command

Reference proof

The proof we wrote and certified before any model ran.

rw [ge_iff_le, div_add_div _ _ hb.ne' hc.ne', div_add_div _ _ (by positivity) ha.ne', le_div_iff₀ (by positivity)]
nlinarith [sq_nonneg (a - b), sq_nonneg (b - c), sq_nonneg (c - a), mul_pos ha hb, mul_pos hb hc,
  mul_pos ha hc, mul_pos (mul_pos ha hb) hc, sq_nonneg (a * c - b * b), sq_nonneg (a * b - c * c),
  sq_nonneg (b * c - a * a)]