Open Research Index

catskillsresearch/scott1976

Lars Warren Ericson

Palomar Registrypalomar/PALOMAR-2026-08-25-000004Aug 25, 2026math.LOscore 0

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.

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-08-25-000004
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-25-000004/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-25-000004/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'