Prove2Me

Probe A

Open
zzProbeParentA

by Zexuan Liu · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

Retired. This was a private, throw-away probe used to isolate a verification-harness failure on theorems whose preamble contains a local def; it has no mathematical content and no replacement node.

Preamble
import Mathlib

def zzStep (n : ℕ) : ℕ :=
  n + 1
Formal statement
theorem zzProbeParentA (n : ℕ) (hn : 0 < n) :
    ∃ m : ℕ, zzStep^[m] n = n + m := by
  sorry

View graph