Theorems / novel_set_07

Authored

Sets · medium

Statement, exactly as the model and Lean see it
theorem lg_target : (Finset.filter (fun n => n % 3 = 0) (Finset.range 30)).card = 10 := 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.

Verified0 model calls · 1 Lean checks · $0.00000

Attempts

  1. attempt 1Verified
    Proof
    rfl

Verified proof

theorem lg_target : (Finset.filter (fun n => n % 3 = 0) (Finset.range 30)).card = 10 := by
  rfl

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

Reference proof

The proof we wrote and certified before any model ran.

decide