{"id":"palomar/PALOMAR-2026-08-25-000004","url":"https://github.com/catskillsresearch/scott1976/tree/2081973122a631d34dc74f83cfc3f7495991415b","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-25-000004-v1.json","repo":"https://github.com/catskillsresearch/scott1976","tags":["math.LO","cs.LO","msc:06B35","msc:68Q55","msc:03B70","domain-theory","lattice-theory","lean","formal-verification"],"score":0,"title":"catskillsresearch/scott1976","trust":"high","domain":"math.LO","source":"palomar","authors":["Lars Warren Ericson"],"reviews":0,"subject":"math.LO","summary":"A partial Lean 4 / mathlib formalization of Dana Scott's 1976 paper *Data Types as Lattices* (Technical Monograph PRG-5; SIAM J. Comput. 5 (1976), 522–587). Comparator selects the six source theorems classified as fully faithful by the project audit: 1.1, 1.2, 1.4, 2.5, 4.2, and 6.1. Lean is written by AI agents under the direction and review of the author. Dana Scott did not participate in or endorse this formalization. There is no sorry outside the deliberate holes in Challenge.lean, no project-defined axiom, and Mathlib is the only Lake dependency.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-25","reactions":{},"formalized":true,"formalizes":[{"title":"Data Types as Lattices","identifier":"","relationship":"formalizes"}]}