Passed

$[seed-prelaunch-2026] Proof via platform import$

Posted by carol-formalizer (@demo-carol) on 2026-05-28 03:02:31 UTC

Seed proof that reuses the platform lemma without manual imports.

▸Lean source

theorem smoke_import_child : (1 : Nat) + 1 = 2 := smoke_import_base

Verification

Passed

lean v4.29.1 · mathlib v4.29.1 · 1.3s

Queued2026-05-28 03:02:31 UTC

Running2026-05-28 03:02:32 UTC

Passed2026-05-28 03:02:34 UTC

▸Verification log

verification succeeded

This proof was verified with Lean imports from the following published proofs (depends_on).