Theorems / novel_fun_04

Authored

Functions · medium

Statement, exactly as the model and Lean see it
theorem lg_target (f : ℝ → ℝ) (hf : ∀ x y, f (x + y) = f x + f y) : f 0 = 0 := by
Source
Written for LeanGraph, reference proof certified
Premises used by the reference proof
35

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

Attempts

  1. sample 0 · round 0Type mismatch2.2 s model time
    Proof
    have h0 : f 0 = f (0 + 0) := rfl
rw [hf 0 0] at h0
rw [h0]
    What Lean printed (this is all the model sees on repair)
    4:31: error: Type mismatch
  rfl
has type
  ?m.30 = ?m.30
but is expected to have type
  f 0 = f (0 + 0)

Reference proof

The proof we wrote and certified before any model ran.

have h := hf 0 0
simp at h
linarith