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} \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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2606.30782
curl -X POST /api/v1/records/arxiv/2606.30782/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2606.30782/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'