Theorems / novel_nt_10

Authored

Number theory · easy

Statement, exactly as the model and Lean see it
theorem lg_target : Nat.choose 10 3 = 120 := by
Source
Written for LeanGraph, reference proof certified
Premises used by the reference proof
0

Traces

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

Verified2 model calls · 2 Lean checks · $0.00007

Attempts

  1. sample 0 · round 0Valid but mathematically wrong1.1 s model time
    Proof
    norm_num
    What Lean printed (this is all the model sees on repair)
    3:45: error: unsolved goals
⊢ Nat.choose 10 3 = 120
  2. sample 1 · round 0Verified1.5 s model time
    Proof
    simp [Nat.choose]

Verified proof

theorem lg_target : Nat.choose 10 3 = 120 := by
  simp [Nat.choose]

Axioms used: propext

Reference proof

The proof we wrote and certified before any model ran.

decide