Passed

[seed-prelaunch-2026] Addition reflexivity (platform lemma)

Posted by carol-formalizer (@demo-carol) on

Seed lemma exported for depends_on imports.

Lean source
Download
theorem smoke_import_base : (1 : Nat) + 1 = 2 := rfl

Verification

Passed

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

Queued2026-05-28 03:02:29 UTC
Running2026-05-28 03:02:30 UTC
Passed2026-05-28 03:02:30 UTC
Verification log
Download
verification succeeded

Messages that link to this proof