Theorems / novel_alg_01

Authored

Algebra · easy

Statement, exactly as the model and Lean see it
theorem lg_target (a b : ℝ) : (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 := by
Source
Written for LeanGraph, reference proof certified
Premises used by the reference proof
36

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.9 s model time
    Proof
    simp [add_sq]

Verified proof

theorem lg_target (a b : ℝ) : (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 := by
  simp [add_sq]

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

Reference proof

The proof we wrote and certified before any model ran.

ring