A Lean 4 Formalization of Scott's \emph{Continuous Lattices} (1972)

Lars Warren Ericson

arxiv: 2606.30782 · v1 · pith:D3NADOEXnew · submitted 2026-06-29 · 💻 cs.LO · math.LO

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

Lars Warren Ericson This is my paper

Pith reviewed 2026-07-01 01:42 UTC · model grok-4.3

classification 💻 cs.LO math.LO

keywords continuous latticesLean 4formalizationScott topologylambda calculusdomain theoryinverse limitsway-below relation

0 comments

The pith

Lean 4 contains a complete formalization of the 43 main results from Scott's 1972 continuous lattices paper.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper delivers a machine-checked formalization in Lean 4 of Dana Scott's 1972 development of continuous lattices as models for the lambda calculus. It verifies all 43 numbered results from the first four sections as sorry-free theorems, including the equivalence of injective T0-spaces with continuous lattices and the construction of the inverse limit D_infinity. This work follows Scott's original proof order and incorporates the Milner correction from the same year. A reader would care because it provides a verified foundation for domain-theoretic models used in semantics of programming languages.

Core claim

The formalization shows that Scott's topological definition of injective spaces coincides with order-theoretic continuous lattices, that function spaces and products preserve the structure, and that the inverse limit of the function space tower satisfies D_infinity isomorphic to its own function space, thereby modeling the untyped lambda calculus.

What carries the argument

The inverse limit D_infinity of the function-space tower together with the maps i_infinity and j_infinity that establish the isomorphism D_infinity ≅ [D_infinity → D_infinity].

If this is right

The Scott topology on a continuous lattice is generated by the way-below relation.
Products, function spaces, projections, and retractions of continuous lattices remain continuous lattices.
The inverse limit D_infinity satisfies the fixed-point equation D_infinity ≅ [D_infinity → D_infinity].
All 43 results are available as classical Lean theorems that may be used in further developments.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The formalization could serve as a base for mechanically checking applications of continuous lattices in programming-language semantics.
It may be extended to cover additional sections of Scott's paper or related results in domain theory.
Integration with other Lean libraries on order theory could produce larger verified constructions involving recursive domains.

Load-bearing premise

The Lean definitions and proofs accurately capture the original 1972 statements and the March 1972 Milner correction without material deviation in the interpretation of topological or order-theoretic notions.

What would settle it

A side-by-side comparison that identifies a mismatch in meaning between any of the 43 formalized Lean statements and the corresponding numbered result in Scott's paper.

read the original abstract

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 \(\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_\infty\) of function-space approximants and proves \(D_\infty \cong [D_\infty \to D_\infty]\), yielding a purely mathematical model for Church's untyped \(\lambda\)-calculus. Our development formalizes \textbf{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 \textbf{classical} (uses \texttt{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]}\).

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

Lean formalization of Scott 1972 claims 43 sorry-free theorems but gives no code or repo, so the central claim stays uncheckable.

read the letter

The paper delivers a Lean 4 formalization of the core results in Scott's 1972 Continuous Lattices, including the Milner correction. It states that 43 numbered propositions, lemmas, and theorems from sections 1-4 are proved without sorries, along with the supporting pieces like step functions, the Uparrow basis, and the i_infty/j_infty construction that leads to the D_infty fixed point.

What stands out is the close tracking of Scott's original order of development and the explicit notes in section 5 on where Lean required interpretive choices not spelled out in the 1972 text. That kind of documentation is helpful for anyone who might want to reuse or extend the work. The choice to stay classical and to use only the standard three axioms is also clear and consistent.

The obvious limitation is that the manuscript contains no link to a repository, no attached .lean files, and no way to inspect the actual definitions or run the proofs. Without those, there is no independent way to confirm the theorem count, the absence of sorries, or how faithfully the Lean statements match Scott's topological and order-theoretic notions. For a paper whose main contribution is the formalization itself, this is a material gap rather than a minor omission.

The work is aimed at people already interested in machine-checked domain theory or in preserving landmark results from the 1970s. A reader looking for new mathematical insight will not find it; a reader who wants a verified library to build on will need the code first.

I would not send this to referees until the Lean development is publicly available and the abstract or introduction points to it. Once the code is there, the paper would be worth a serious look because the underlying claim is narrow and checkable.

Referee Report

1 major / 1 minor

Summary. The paper claims to deliver a complete, sorry-free Lean 4 formalization (against mathlib) of 43 numbered results from Sections 1–4 of Scott’s 1972 paper on continuous lattices, incorporating the March 1972 Milner correction; the development includes supporting definitions (step functions, ↑a basis, i∞/j∞ pair, function-space tower) and records interpretive choices in Section 5, with all proofs checking under the footprint [propext, Classical.choice, Quot.sound].

Significance. A verified formalization of this landmark construction would supply a reusable, machine-checked reference for the equivalence of injective T0-spaces and continuous lattices, the inverse-limit model D∞ ≅ [D∞ → D∞], and related results in domain theory, thereby supporting further formal work on denotational semantics and lambda-calculus models.

major comments (1)

[Abstract and Section 5] Abstract and Section 5: the central claim that 43 numbered results have been formalized as sorry-free theorems cannot be assessed, because the manuscript supplies no repository URL, GitHub link, or supplementary .lean files. Without the actual definitions and proof scripts, neither the count of 43 results, the absence of sorries, nor the fidelity of the Lean notions (including the interpretation of the Milner correction) to the 1972 text can be confirmed; this is load-bearing for the paper’s contribution.

minor comments (1)

[Abstract] The abstract refers to “Milner’s coarser-than-Scott hypothesis” and “the i∞/j∞ pair” without a brief inline gloss or forward reference to their Lean definitions, which may hinder readers who have not yet consulted the code.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their review and for emphasizing the need for verifiable access to the formalization. We address the single major comment below.

read point-by-point responses

Referee: [Abstract and Section 5] Abstract and Section 5: the central claim that 43 numbered results have been formalized as sorry-free theorems cannot be assessed, because the manuscript supplies no repository URL, GitHub link, or supplementary .lean files. Without the actual definitions and proof scripts, neither the count of 43 results, the absence of sorries, nor the fidelity of the Lean notions (including the interpretation of the Milner correction) to the 1972 text can be confirmed; this is load-bearing for the paper’s contribution.

Authors: We agree that the submitted manuscript omitted a repository link, making independent assessment of the 43 theorems impossible from the text alone. This was an oversight on our part. The complete Lean 4 development (against mathlib) is maintained in a public repository and contains precisely the 43 sorry-free theorems for the numbered results from Sections 1–4, the supporting infrastructure (step functions, ↑a basis, i∞/j∞ pair, function-space tower), and the notes on interpretive choices and the Milner correction that appear in Section 5. All proofs check under the stated footprint. In the revised manuscript we will insert a prominent URL to the repository in both the abstract and Section 5, together with build instructions, so that the count, absence of sorries, and fidelity to Scott’s text can be directly confirmed. revision: yes

Circularity Check

0 steps flagged

No significant circularity: formalization of external 1972 source

full rationale

The paper claims a Lean 4 formalization of 43 numbered results from Scott's external 1972 paper (including Milner correction), presented as sorry-free theorems with supporting infrastructure. No self-definitional loops, fitted parameters renamed as predictions, load-bearing self-citations, uniqueness theorems imported from the same authors, ansatzes smuggled via citation, or renamings of known results appear in the derivation chain. The central claim reduces to matching an independent external benchmark rather than any internal construction or fit. This is the most common honest non-finding for formalization papers; the absence of a code repository affects verifiability but does not create circularity under the enumerated patterns.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The formalization rests on mathlib and the axiom of choice; no free parameters or invented entities are introduced.

axioms (1)

standard math Classical.choice
Used transitively; explicitly noted in the abstract as part of the classical development.

pith-pipeline@v0.9.1-grok · 5892 in / 1165 out tokens · 44811 ms · 2026-07-01T01:42:27.186789+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

13 extracted references

[1]

Suprema are inherited from`[D -> D]`; infima are derived by` completeLatticeOfSup`

Lattice D] : Type _ := {j : ScottMap D D // IsProjection j} namespace Projections noncomputable instance instSupSet : SupSet (Projections D) := <fun T => <sSup (Set.image Subtype.val T), isProjection_sSup (by rintro j <p, _, rfl>; exact p.2)>> theorem isLUB_sSup (T : Set (Projections D)) : IsLUB T (sSup T) := by constructor * intro p hp apply Subtype.coe_...

1972
[2]

-/ def Compatible (x : forall n, D n) : Prop := forall n, (P n).retr (x (n + 1)) = x n /-- **Scott 1972, S4.** The inverse limit`D_ inf`as the subspace of compatible sequences

-> D n) := by intro x y constructor * intro h have h':= (P n).retr.monotone h rwa [(P n).retr_incl] at h' * intro h exact le_trans ((P n).incl.monotone h) ((P n).incl_retr_le y) /-- Compatibility of a sequence:`j_n(x_{n+1}) = x_n`for all`n`. -/ def Compatible (x : forall n, D n) : Prop := forall n, (P n).retr (x (n + 1)) = x n /-- **Scott 1972, S4.** The ...

1972
[3]

=> (P k).retr z) := funext (fun x => projLE_succ D P hk (Nat.le_succ_of_le hk) x) rw [hfun] exact ScottMap.preservesDirectedSup_comp ih (fun S hS hd => (P k).retr.preservesDirectedSup_coe S hS hd) theorem iComp_preservesDirectedSup (n m : Nat) : PreservesDirectedSup (fun x : D n => iComp D P n x m) := by by_cases h : n <= m * have hfun : (fun x : D n => i...

1972
[4]

the remark following 4.2

:= (P n).incl_retr_le _) theorem embInf_family_directed (x : InverseLimit D P) : DirectedOn (* <= *) (Set.range (fun n => embInf D P n (x.1 n))) := directedOn_range.2 (monotone_nat_of_le_succ (embInf_le_succ D P x)).directed_le /-- **Scott 1972, S4.** Each`x in D_ inf`is the (monotone) lub of its projections: `x = bigcup _n i_{n inf }(x_n)`. -/ theorem in...

1972
[5]

-/ theorem coconeInf_comp_embInf (f : forall n, ScottMap (D n) D') (hf : forall n x, f n x = f (n +

x := (f (k + 1)).monotone ((P k).incl_retr_le x) /-- **Scott 1972, Corollary 4.3 (factorization).**`f_n = f inf comp i_{n inf }`. -/ theorem coconeInf_comp_embInf (f : forall n, ScottMap (D n) D') (hf : forall n x, f n x = f (n +

1972
[6]

((P n).incl x)) (n : Nat) (x : D n) : coconeInf D P f (embInf D P n x) = f n x := by apply le_antisymm * show ( bigcup m, f m ((embInf D P n x).1 m)) <= f n x refine iSup_le fun m => ?_ 91 show f m (iComp D P n x m) <= f n x by_cases h : n <= m * rw [iComp_of_le D P h]; exact le_of_eq (coconeInf_climb D P f hf x h) * rw [iComp_of_ge D P h]; exact coconeIn...

1972
[7]

((P n).incl x)) : exists ! g : ScottMap (InverseLimit D P) D', forall n x, f n x = g (embInf D P n x) := by refine <<coconeInf D P f, continuous_of_preservesDirectedSup (coconeInf_preservesDirectedSup D P f)>, ?_, ?_> * exact fun n x => (coconeInf_comp_embInf D P f hf n x).symm * intro g hg ext x --`g x = f inf x`, since`x = bigcup _n i_{n inf }(x_n)`and`...

1972
[8]

= ScottMap (towerType D_0 n) (towerType D_0 n) := rfl /-- View an element of`D_{n+1}`as the Scott map`[D_n -> D_n]`it definitionally is. -/ def towerToMap {D_0 : CLat.{u}} {n : Nat} (f : towerType D_0 (n + 1)) : ScottMap (towerType D_0 n) (towerType D_0 n) := f /-- Apply an element of`D_{n+1}`as a function`D_n -> D_n`(definitional via` towerType_succ`). -...

1972
[9]

= (towerProj D_0 j_0 n).functionSpace := rfl section Tower variable (D_0 : CLat.{u}) (j_0 : IsContinuousLatticeProjection D_0.carrier (ScottMap D_0.carrier D_0.carrier)) /-- **Scott 1972, S4 (recursion for the embeddings).**`i_{n+1}(x) = i_n comp x comp j_n`. -/ theorem towerProj_succ_incl_apply (n : Nat) (x : towerType D_0 (n + 1)) (y : towerType D_0 (n ...

1972
[10]

Scott- continuous as a supremum of the Scott maps `jInfTerm n`

(conjMap (projInf (towerType D_0) (towerProj D_0 j_0) n) (embInf (towerType D_0) (towerProj D_0 j_0) n) f) := rfl /-- **Scott 1972, S4 (Theorem 4.4).** The projection`j_ inf : [D_ inf -> D_ inf ] -> D_ inf`, `j_ inf (f) = bigcup _n i_{(n+1) inf }(j_{ inf n} comp f comp i_{n inf })`. Scott- continuous as a supremum of the Scott maps `jInfTerm n`. -/ noncom...

1972
[11]

(conjMap_incl_le_conjMap_succ D_0 j_0 n (iInfTerm D_0 j_0 m x)) have g_mono_n (m : Nat) : Monotone (fun n => g n m) := monotone_nat_of_le_succ (g_mono_n_succ m) have hin : ( bigcup n, jInfTerm D_0 j_0 n (embInfInf D_0 j_0 x)) = bigcup n, bigcup m, g n m := by congr 1 funext n exact hinner n rw [hin, iSup_2_monotone_eq_diagonal g g_mono_m g_mono_n] congr 1...

1972
[12]

((towerProj D_0 j_0 n).incl y)))) = projInf (towerType D_0) (towerProj D_0 j_0) n (f (embInf (towerType D_0) (towerProj D_0 j_0) n y)) rw [embInf_succ (towerType D_0) (towerProj D_0 j_0) n y] exact (f (embInf (towerType D_0) (towerProj D_0 j_0) n y)).2 n /-- **Scott 1972, S4 (Theorem 4.4, second half).**`i_ inf comp j_ inf = id`on`[D_ inf -> D_ inf ]`. -/...

1972
[13]

= conjMap (projInf (towerType D_0) (towerProj D_0 j_0) n) (embInf (towerType D_0) (towerProj D_0 j_0) n) f := by intro n rw [hpi] exact lemma_4_5 (towerType D_0) (towerProj D_0 j_0) (fun k => conjMap (projInf (towerType D_0) (towerProj D_0 j_0) k) (embInf (towerType D_0) (towerProj D_0 j_0) k) f) (fun m => towerProj_retr_conjMap_succ D_0 j_0 m f) n -- Eva...

1972

[1] [1]

Suprema are inherited from`[D -> D]`; infima are derived by` completeLatticeOfSup`

Lattice D] : Type _ := {j : ScottMap D D // IsProjection j} namespace Projections noncomputable instance instSupSet : SupSet (Projections D) := <fun T => <sSup (Set.image Subtype.val T), isProjection_sSup (by rintro j <p, _, rfl>; exact p.2)>> theorem isLUB_sSup (T : Set (Projections D)) : IsLUB T (sSup T) := by constructor * intro p hp apply Subtype.coe_...

1972

[2] [2]

-/ def Compatible (x : forall n, D n) : Prop := forall n, (P n).retr (x (n + 1)) = x n /-- **Scott 1972, S4.** The inverse limit`D_ inf`as the subspace of compatible sequences

-> D n) := by intro x y constructor * intro h have h':= (P n).retr.monotone h rwa [(P n).retr_incl] at h' * intro h exact le_trans ((P n).incl.monotone h) ((P n).incl_retr_le y) /-- Compatibility of a sequence:`j_n(x_{n+1}) = x_n`for all`n`. -/ def Compatible (x : forall n, D n) : Prop := forall n, (P n).retr (x (n + 1)) = x n /-- **Scott 1972, S4.** The ...

1972

[3] [3]

=> (P k).retr z) := funext (fun x => projLE_succ D P hk (Nat.le_succ_of_le hk) x) rw [hfun] exact ScottMap.preservesDirectedSup_comp ih (fun S hS hd => (P k).retr.preservesDirectedSup_coe S hS hd) theorem iComp_preservesDirectedSup (n m : Nat) : PreservesDirectedSup (fun x : D n => iComp D P n x m) := by by_cases h : n <= m * have hfun : (fun x : D n => i...

1972

[4] [4]

the remark following 4.2

:= (P n).incl_retr_le _) theorem embInf_family_directed (x : InverseLimit D P) : DirectedOn (* <= *) (Set.range (fun n => embInf D P n (x.1 n))) := directedOn_range.2 (monotone_nat_of_le_succ (embInf_le_succ D P x)).directed_le /-- **Scott 1972, S4.** Each`x in D_ inf`is the (monotone) lub of its projections: `x = bigcup _n i_{n inf }(x_n)`. -/ theorem in...

1972

[5] [5]

-/ theorem coconeInf_comp_embInf (f : forall n, ScottMap (D n) D') (hf : forall n x, f n x = f (n +

x := (f (k + 1)).monotone ((P k).incl_retr_le x) /-- **Scott 1972, Corollary 4.3 (factorization).**`f_n = f inf comp i_{n inf }`. -/ theorem coconeInf_comp_embInf (f : forall n, ScottMap (D n) D') (hf : forall n x, f n x = f (n +

1972

[6] [6]

((P n).incl x)) (n : Nat) (x : D n) : coconeInf D P f (embInf D P n x) = f n x := by apply le_antisymm * show ( bigcup m, f m ((embInf D P n x).1 m)) <= f n x refine iSup_le fun m => ?_ 91 show f m (iComp D P n x m) <= f n x by_cases h : n <= m * rw [iComp_of_le D P h]; exact le_of_eq (coconeInf_climb D P f hf x h) * rw [iComp_of_ge D P h]; exact coconeIn...

1972

[7] [7]

((P n).incl x)) : exists ! g : ScottMap (InverseLimit D P) D', forall n x, f n x = g (embInf D P n x) := by refine <<coconeInf D P f, continuous_of_preservesDirectedSup (coconeInf_preservesDirectedSup D P f)>, ?_, ?_> * exact fun n x => (coconeInf_comp_embInf D P f hf n x).symm * intro g hg ext x --`g x = f inf x`, since`x = bigcup _n i_{n inf }(x_n)`and`...

1972

[8] [8]

= ScottMap (towerType D_0 n) (towerType D_0 n) := rfl /-- View an element of`D_{n+1}`as the Scott map`[D_n -> D_n]`it definitionally is. -/ def towerToMap {D_0 : CLat.{u}} {n : Nat} (f : towerType D_0 (n + 1)) : ScottMap (towerType D_0 n) (towerType D_0 n) := f /-- Apply an element of`D_{n+1}`as a function`D_n -> D_n`(definitional via` towerType_succ`). -...

1972

[9] [9]

= (towerProj D_0 j_0 n).functionSpace := rfl section Tower variable (D_0 : CLat.{u}) (j_0 : IsContinuousLatticeProjection D_0.carrier (ScottMap D_0.carrier D_0.carrier)) /-- **Scott 1972, S4 (recursion for the embeddings).**`i_{n+1}(x) = i_n comp x comp j_n`. -/ theorem towerProj_succ_incl_apply (n : Nat) (x : towerType D_0 (n + 1)) (y : towerType D_0 (n ...

1972

[10] [10]

Scott- continuous as a supremum of the Scott maps `jInfTerm n`

(conjMap (projInf (towerType D_0) (towerProj D_0 j_0) n) (embInf (towerType D_0) (towerProj D_0 j_0) n) f) := rfl /-- **Scott 1972, S4 (Theorem 4.4).** The projection`j_ inf : [D_ inf -> D_ inf ] -> D_ inf`, `j_ inf (f) = bigcup _n i_{(n+1) inf }(j_{ inf n} comp f comp i_{n inf })`. Scott- continuous as a supremum of the Scott maps `jInfTerm n`. -/ noncom...

1972

[11] [11]

(conjMap_incl_le_conjMap_succ D_0 j_0 n (iInfTerm D_0 j_0 m x)) have g_mono_n (m : Nat) : Monotone (fun n => g n m) := monotone_nat_of_le_succ (g_mono_n_succ m) have hin : ( bigcup n, jInfTerm D_0 j_0 n (embInfInf D_0 j_0 x)) = bigcup n, bigcup m, g n m := by congr 1 funext n exact hinner n rw [hin, iSup_2_monotone_eq_diagonal g g_mono_m g_mono_n] congr 1...

1972

[12] [12]

((towerProj D_0 j_0 n).incl y)))) = projInf (towerType D_0) (towerProj D_0 j_0) n (f (embInf (towerType D_0) (towerProj D_0 j_0) n y)) rw [embInf_succ (towerType D_0) (towerProj D_0 j_0) n y] exact (f (embInf (towerType D_0) (towerProj D_0 j_0) n y)).2 n /-- **Scott 1972, S4 (Theorem 4.4, second half).**`i_ inf comp j_ inf = id`on`[D_ inf -> D_ inf ]`. -/...

1972

[13] [13]

= conjMap (projInf (towerType D_0) (towerProj D_0 j_0) n) (embInf (towerType D_0) (towerProj D_0 j_0) n) f := by intro n rw [hpi] exact lemma_4_5 (towerType D_0) (towerProj D_0 j_0) (fun k => conjMap (projInf (towerType D_0) (towerProj D_0 j_0) k) (embInf (towerType D_0) (towerProj D_0 j_0) k) f) (fun m => towerProj_retr_conjMap_succ D_0 j_0 m f) n -- Eva...

1972