Inequalities · medium

Statement, exactly as the model and Lean see it

theorem lg_target (a b : ℝ) (ha : 0 < a) (hb : 0 < b) : (a + b) * (1 / a + 1 / b) ≥ 4 := by

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

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.00010

Attempts

sample 0 · round 0Syntax error3.4 s model time

Proof

simp only [mul_add, add_mul, one_div] at *,
apply (add_right_inj (1 / a + 1 / b)) at *,
have h : (a * b) * (1 / a + 1 / b) = b + a := by simp,
rw h,
apply mul_le_of_nonneg_right (b + a) (a * b),
apply mul_nonneg,
exact ha,
exact hb,
apply add_nonneg ha hb,
apply le_trans (mul_self_le_sq (a * b)) (add_le_add_left (a * b) (a * b)),
apply mul_le_mul ha hb ha hb,
apply le_refl

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

3:89: error: unsolved goals
a b : ℝ
ha : 0 < a
hb : 0 < b
⊢ a * a⁻¹ + b * a⁻¹ + (a * b⁻¹ + b * b⁻¹) ≥ 4
4:44: error: unexpected token ','; expected command

Reference proof

The proof we wrote and certified before any model ran.

have h : (a + b) * (1 / a + 1 / b) = 2 + a / b + b / a := by field_simp; ring
have h2 : a / b + b / a ≥ 2 := by
  rw [ge_iff_le, div_add_div _ _ hb.ne' ha.ne', le_div_iff₀ (by positivity)]
  nlinarith [sq_nonneg (a - b)]
linarith