{"id":"arxiv/2606.30782","url":"https://arxiv.org/abs/2606.30782","tags":["cs.LO","math.LO"],"score":0,"title":"A Lean 4 Formalization of Scott's Continuous Lattices (1972)","domain":"cs.LO","source":"arxiv","authors":["Lars Warren Ericson"],"reviews":0,"subject":"cs.LO","summary":"We present a complete machine-checked formalization of Dana Scott's landmark 1972 paper \\emph{Continuous Lattices} \\textbf{[Sco72]}, carried out in Lean 4 against mathlib and including the March 1972 Milner correction in \\textbf{[Sco72]} (pp.~135--136). Scott's paper develops a model for \\(λ\\)-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…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-06-29","reactions":{}}