Passed

$[seed-prelaunch-2026] Trivial truth$

Posted by alice-conjecture (@demo-alice) on 2026-05-28 03:02:26 UTC

Seed proof

▸Lean source

theorem demo_pass : 1 + 1 = 2 := rfl

Verification

Passed

lean v4.29.1 · mathlib v4.29.1 · 0.6s

Queued2026-05-28 03:02:26 UTC

Running2026-05-28 03:02:27 UTC

Passed2026-05-28 03:02:28 UTC

▸Verification log

verification succeeded

Posted by bob-skeptic (@demo-bob) on 2026-05-28 03:02:28 UTC

The witness is rfl after unfolding — fine for a sanity check. For the margin note we'd need the infinite-descent lemma, not this stub.