Help a new user out

Stream: new members

[Alphara]

hey there, i m looking for some help and I don't really know where to get it. I'm trying to prove Nesbitt's inequality but I hardly have any LEAN knowledge so I was testing if an LLM like Gemini can come up with a proof (not sure how much popularity ai assistance has here) but it came down to this:

image.png

import Mathlib.Data.Real.Basic
import Mathlib.Analysis.MeanInequalities -- Contains the key inequality
import Mathlib.Tactic.Positivity -- For proving terms are positive

-- Let a, b, c be positive real numbers
variable (a b c : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)

-- Nesbitt's Inequality: a/(b+c) + b/(c+a) + c/(a+b) ≥ 3/2
example : 3 / 2 ≤ a / (b + c) + b / (a + c) + c / (a + b) := by
  -- Let x = b+c, y = c+a, z = a+b. These are the denominators.
  let x := b + c
  let y := c + a
  let z := a + b

  -- We need to prove that these new variables are positive.
  -- The `positivity` tactic can do this automatically.
  have hx_pos : 0 < x := by positivity
  have hy_pos : 0 < y := by positivity
  have hz_pos : 0 < z := by positivity

  -- The key step is applying the AM-HM inequality, which in Mathlib is
  -- called `sum_mul_inv_sum_ge_sq`. It states that for positive x, y, z:
  -- (x + y + z) * (1/x + 1/y + 1/z) ≥ 3^2 = 9
  -- We create a helper lemma `h` with this fact.
  have h : (x + y + z) * (1/x + 1/y + 1/z) ≥ 9 := by
    -- We need to provide the list of numbers [x, y, z] as a vector.
    let v : Fin 3 → ℝ := ![x, y, z]
    -- And we need to show all elements of the vector are positive.
    have hv_pos : ∀ i, 0 < v i := by
      -- This is a bit of boilerplate to check each element.
      intro i; fin_cases i <;> simp <;> assumption
    -- Now apply the main theorem from Mathlib.
    exact sum_mul_inv_sum_ge_sq v hv_pos

  -- At this point, `h` is the inequality:
  -- `(b+c + c+a + a+b) * (1/(b+c) + 1/(c+a) + 1/(a+b)) ≥ 9`
  -- The rest of the proof is just algebra, which `linarith` can solve.
  -- We give `h` as a hypothesis to `linarith`.
  linarith [h]

if anyone could help I'd be really thankful. Thanks in advance.

[Alphara]

hey there, i m looking for some help and I don't really know where to get it. I'm trying to prove Nesbitt's inequality but I hardly have any LEAN knowledge so I was testing if an LLM like Gemini can come up with a proof (not sure how much popularity ai assistance has here) but it came down to this:

image.png

import Mathlib.Data.Real.Basic
import Mathlib.Analysis.MeanInequalities -- Contains the key inequality
import Mathlib.Tactic.Positivity -- For proving terms are positive

-- Let a, b, c be positive real numbers
variable (a b c : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)

-- Nesbitt's Inequality: a/(b+c) + b/(c+a) + c/(a+b) ≥ 3/2
example : 3 / 2 ≤ a / (b + c) + b / (a + c) + c / (a + b) := by
  -- Let x = b+c, y = c+a, z = a+b. These are the denominators.
  let x := b + c
  let y := c + a
  let z := a + b

  -- We need to prove that these new variables are positive.
  -- The `positivity` tactic can do this automatically.
  have hx_pos : 0 < x := by positivity
  have hy_pos : 0 < y := by positivity
  have hz_pos : 0 < z := by positivity

  -- The key step is applying the AM-HM inequality, which in Mathlib is
  -- called `sum_mul_inv_sum_ge_sq`. It states that for positive x, y, z:
  -- (x + y + z) * (1/x + 1/y + 1/z) ≥ 3^2 = 9
  -- We create a helper lemma `h` with this fact.
  have h : (x + y + z) * (1/x + 1/y + 1/z) ≥ 9 := by
    -- We need to provide the list of numbers [x, y, z] as a vector.
    let v : Fin 3 → ℝ := ![x, y, z]
    -- And we need to show all elements of the vector are positive.
    have hv_pos : ∀ i, 0 < v i := by
      -- This is a bit of boilerplate to check each element.
      intro i; fin_cases i <;> simp <;> assumption
    -- Now apply the main theorem from Mathlib.
    exact sum_mul_inv_sum_ge_sq v hv_pos

  -- At this point, `h` is the inequality:
  -- `(b+c + c+a + a+b) * (1/(b+c) + 1/(c+a) + 1/(a+b)) ≥ 9`
  -- The rest of the proof is just algebra, which `linarith` can solve.
  -- We give `h` as a hypothesis to `linarith`.
  linarith [h]

if anyone could help I'd be really thankful. Thanks in advance.

[Kenny Lau]

do you want help learning lean, or do you want somone to fix your LLM output for you

[Alphara]

to be honest I want to put in the time to learn, which I'm willing to do soon enough, but I wanted to have this LLM output corrected to showcase it shortly

[Alphara]

As my understanding goes, the sum_mul_inv_sum_ge_sq is the culprit and is from a previous LEAN version?

[Notification Bot]

This topic was moved here from #lean4 > Help a new user out by Kevin Buzzard.

[Kevin Buzzard]

sum_mul_inv_sum_ge_sq is a hallucination, as one might expect from an LLM. Do you know a maths proof of this result? Maybe you could vibe code your way through that.

If you want to learn Lean then definitely don't do it like the way you're doing. You might get to the end of the proof with unidiomatic code, and if that's the win you're looking for then you'll probably get it in the end, but I'm not sure what it will teach you.

[Notification Bot]

A message was moved here from #new members > Implicit coercion of type doesn't take place by Kevin Buzzard.

[Kevin Buzzard]

PS please don't double post

[Alphara]

I see, thanks. I'm usually against vibe code but I figured I should try and see the state of AI for LEAN, since there's been a couple endeavors I've heard of that worked quite well, but I suppose those were pretty cherry picked. Figured a textbook proof could be formalized from a prompt to an LLM but I guess that's fiction lol. Anywho, I'm willing to put in the effort to learn, thanks for the thoughtful response and PS on how to use the zulip platform, it's a first with that for me as well.