Inequalities · easy

Statement, exactly as the model and Lean see it

theorem lg_target (x y : ℝ) (hx : 0 ≤ x) (hy : 0 ≤ y) (h : x + y = 2) : x * y ≤ 1 := by

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

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

Attempts

sample 0 · round 0Syntax error9.9 s model time

Proof

have hxy : x * y ≤ 1 := by
  have h1 : x + y = 2 := h
  have h2 : (x - 1) * (y - 1) ≥ 0 :=
    by rw [h1]; simp only [mul_sub, sub_add, add_sub, mul_left_distrib, mul_right_distrib, add_mul, one_add]
    exact (add_nonneg (le_refl 1) (le_refl 1)).trans (mul_nonneg (le_zero (by rwa le_add_right at h1)) (le_zero (by rwa le_add_right at h1)))
  rw [mul_sub, sub_add, add_sub, mul_left_distrib, mul_right_distrib, add_mul, one_add] at h2
  rw [h1] at h2
  exact h2.trans (le_add_right 1 1)

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

7:13: error: Tactic `rewrite` failed: Did not find an occurrence of the pattern
  x + y
in the target expression
  (x - 1) * (y - 1) ≥ 0

x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h h1 : x + y = 2
⊢ (x - 1) * (y - 1) ≥ 0
4:26: error: unsolved goals
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h h1 : x + y = 2
h2 : (x - 1) * (y - 1) ≥ 0
⊢ x * y ≤ 1
3:85: error: unsolved goals
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h : x + y = 2
hxy : x * y ≤ 1
⊢ x * y ≤ 1
8:6: error: unexpected identifier; expected command

Reference proof

The proof we wrote and certified before any model ran.

nlinarith [sq_nonneg (x - y)]