Theorems / novel_prob_01

Authored

Probability · medium

Statement, exactly as the model and Lean see it
theorem lg_target (p : NNReal) (h : p ≤ 1) : PMF.bernoulli p h true = (p : ENNReal) := by
Source
Written for LeanGraph, reference proof certified
Premises used by the reference proof
1

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 (p : NNReal) (h : p ≤ 1) : PMF.bernoulli p h true = (p : ENNReal) := by
  rfl

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

Reference proof

The proof we wrote and certified before any model ran.

simp [PMF.bernoulli_apply]