Theorems / mh_prob_7642f8

Mathlib held-out

Probability · medium

Statement, exactly as the model and Lean see it
theorem lg_target {Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] {X : Ω → E} [NormedSpace ℝ E] (hX : ProbabilityTheory.HasGaussianLaw X P) : ProbabilityTheory.HasGaussianLaw (-X) P := by
Mathlib declaration
ProbabilityTheory.HasGaussianLaw.neg
Held-out module
Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
Banned modules (itself + downstream)
7
Reference proof premises (reachable / held-out)
2 / 1

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 0Hallucinated theorem1.9 s model time
    Proof
    intros
constructor
apply ProbabilityTheory.hasGaussianLaw_neg
exact hX
    What Lean printed (this is all the model sees on repair)
    6:8: error: Unknown identifier `ProbabilityTheory.hasGaussianLaw_neg`
7:2: error: No goals to be solved

Reference proof

Mathlib's own source for this declaration, shown for comparison. It may use lemmas the prover is not allowed to use.

lemma neg (hX : HasGaussianLaw X P) : HasGaussianLaw (-X) P := by simpa using hX.smul (-1)