Lean 4 / Mathlib formalisations for eight open Erdős problems — 68, 243, 249, 251, 257, 269, 1041, 1049. All eight remain open. Follow any of 130 registered claims to its source, its receipts, and the exact point where it stops, in under a second, with no Lean installed. Companion to wcook04/plectis.