We present a complete machine-checked formalization of Dana Scott's landmark 1972 paper Continuous Lattices [Sco72], carried out in Lean 4 against mathlib and including the March 1972 Milner correction in [Sco72] (pp. 135–136). Scott's paper develops a model for \(λ\)-calculus from a topological starting point. He defines injective \(T_0\)-spaces – those with a strong extension property for continuous maps – and shows that they are exactly the continuous lattices: complete lattices whose Scott topology is determined by the order via the way-below relation (\(\ll\)). On this foundation he studies projections, retractions, products, function spaces, and inverse limits. The capstone (Theorem 4.4) constructs an inverse limit \(D_\infty\) of function-space approximants and proves \(D_\infty \cong [D_\infty \to D_\infty]\), yielding a purely mathematical model for Church's untyped \(λ\)-calculus. Our development formalizes 43 numbered results from Scott's Sections 1–4 (Propositions, Corollaries, Lemmas, and Theorems), each as a sorry-free Lean theorem, together with supporting infrastructure (step functions, the \(\Uparrow a\) basis of Scott opens, Milner's coarser-than-Scott hypothesis, the function-space tower, and the \(i_\infty\)/\(j_\infty\) pair). The formalization is classical (uses Classical.choice transitively) and follows Scott's proof dependency order. Where the Lean proof required choices not visible in the original – or where dead ends were encountered – we record detailed notes in Section 5. All proofs check with the standard footprint \(\texttt{[propext, Classical.choice, Quot.sound]}\). The formalization has been accepted into the Palomar registry.