Inequalities · easy

Statement, exactly as the model and Lean see it

theorem lg_target (a b c : ℝ) : a * b + b * c + c * a ≤ a ^ 2 + b ^ 2 + c ^ 2 := by

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

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

Attempts

sample 0 · round 0Syntax error23.6 s model time

Proof

have h1 : a * b ≤ (a^2 + b^2) / 2 := by
  rw [mul_comm]
  apply (le_div_of_mult_le_left (a^2 + b^2) 2)
  exact (add_right_inj (le_refl (a^2 + b^2)) (le_mul_self (abs a) (abs b)))
have h2 : b * c ≤ (b^2 + c^2) / 2 := by
  rw [mul_comm]
  apply (le_div_of_mult_le_left (b^2 + c^2) 2)
  exact (add_right_inj (le_refl (b^2 + c^2)) (le_mul_self (abs b) (abs c)))
have h3 : c * a ≤ (c^2 + a^2) / 2 := by
  rw [mul_comm]
  apply (le_div_of_mult_le_left (c^2 + a^2) 2)
  exact (add_right_inj (le_refl (c^2 + a^2)) (le_mul_self (abs c) (abs a)))
calc
  a * b + b * c + c * a ≤ (a^2 + b^2)/2 + (b^2 + c^2)/2 + (c^2 + a^2)/2
  by rw [h1, h2, h3]
... = (a^2 + b^2 + b^2 + c^2 + c^2 + a^2) / 2
  by simp
... = (2 * a^2 + 2 * b^2 + 2 * c^2) / 2
  by simp
... = a^2 + b^2 + c^2
  by simp

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

19:5: error: unexpected token '='; expected term
6:11: error: Unknown identifier `le_div_of_mult_le_left`
7:4: error: No goals to be solved
10:11: error: Unknown identifier `le_div_of_mult_le_left`
11:4: error: No goals to be solved
14:11: error: Unknown identifier `le_div_of_mult_le_left`
15:4: error: No goals to be solved

Reference proof

The proof we wrote and certified before any model ran.

nlinarith [sq_nonneg (a - b), sq_nonneg (b - c), sq_nonneg (c - a)]