Theorems / novel_alg_09

Authored

Algebra · medium

Statement, exactly as the model and Lean see it
theorem lg_target (x : ℝ) (hx : 0 < x) : Real.log (x ^ 3) = 3 * Real.log x := by
Source
Written for LeanGraph, reference proof certified
Premises used by the reference proof
6

Traces

Each configuration's full record: what was retrieved, what the model wrote, what Lean said back.

Verified1 model calls · 1 Lean checks · $0.00004

Attempts

  1. sample 0 · round 0Verified1.2 s model time
    Proof
    simp [Real.log_pow, hx]

Verified proof

theorem lg_target (x : ℝ) (hx : 0 < x) : Real.log (x ^ 3) = 3 * Real.log x := by
  simp [Real.log_pow, hx]

Axioms used: propext, Classical.choice, Quot.sound

Reference proof

The proof we wrote and certified before any model ran.

rw [Real.log_pow]
norm_num