A Lean 4 Formalization of Scott's Continuous Lattices (1972)

We present a complete machine-checked formalization of Dana Scott’s landmark 1972 paper \emph{Continuous Lattices} $\mathbf{\text{[Sco72]}}$, carried out in Lean 4 against mathlib and including the March 1972 Milner correction in $\mathbf{\text{[Sco72]}}$ (pp.~135–136). Scott’s paper develops a model for $\lambda$-calculus from a topological starting point. He defines \emph{injective} $T_0$-spaces – those with a strong extension property for continuous maps – and shows that they are exactly the \emph{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_{\mathrm{\infty }}$ of function-space approximants and proves $D_{\mathrm{\infty }}\cong [D_{\mathrm{\infty }}\to D_{\mathrm{\infty }}]$, yielding a purely mathematical model for Church’s untyped $\lambda$-calculus. Our development formalizes $\mathbf{\text{43}}\mathbf{\text{numbered}}\mathbf{\text{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_{\mathrm{\infty }}$/$j_{\mathrm{\infty }}$ pair). The formalization is $\mathbf{\text{classical}}$ (uses $\mathtt{\text{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 $\mathtt{\text{[propext,}}\mathtt{\text{Classical.choice,}}\mathtt{\text{Quot.sound]}}$. The formalization has been accepted into the Palomar registry.