Theorems / mh_ineq_f31a9a

Mathlib held-out

Inequalities · easy

Statement, exactly as the model and Lean see it
theorem lg_target (x : ENNReal) (y : ℝ) : x ^ y = (↑y * x.log).exp := by
Mathlib declaration
EReal.ENNReal.rpow_eq_exp_mul_log
Held-out module
Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Banned modules (itself + downstream)
7
Reference proof premises (reachable / held-out)
0 / 1

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

Attempts

  1. sample 0 · round 0Hallucinated theorem1.6 s model time
    Proof
    rw [pow_log, log_def, exp_add, mul_comm, exp_mul]
    What Lean printed (this is all the model sees on repair)
    4:6: error: Unknown identifier `pow_log`
3:70: error: unsolved goals
x : ENNReal
y : ℝ
⊢ x ^ y = (↑y * x.log).exp

Reference proof

Mathlib's own source for this declaration, shown for comparison. It may use lemmas the prover is not allowed to use.

@[deprecated (since := "2026-07-15")] alias _root_.EReal.ENNReal.rpow_eq_exp_mul_log :=
  rpow_eq_exp_mul_log