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

arXiv: https://arxiv.org/abs/2606.30782 · HTML: https://mlsanity.com/paper/2606.30782/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 29 Jun 2026.

## Built on by (most cited first, 1 of 1)

- [ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization](https://mlsanity.com/paper/2609.34960/) (2026)

## Abstract (arXiv)

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 (T0)-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_∞) of function-space approximants and proves (D_∞ cong [D_∞ → D_∞]), 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_∞)/(j_∞) pair). The formalization is classical (uses textttClassical.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.