Open Research Index

catskillsresearch/scott1980

Lars Warren Ericson

Palomar Registrypalomar/PALOMAR-2026-08-24-000001Aug 25, 2026cs.LOscore 0

A Lean 4 / mathlib formalization of Dana Scott's 1980 Oxford lectures, published May 1981 as PRG-19 Lectures on a Mathematical Theory of Computation. The principal sourced Palomar result is the first sentence of Theorem 8.8: the neighbourhood system U over [0,1) ⊆ ℚ is universal, in the sense that every countable neighbourhood system D embeds as a subdomain (D ⊴ U). Comparator also selects two new formal corollaries: P4_embeds for Scott's Example 1.5 and Ssys_embeds for Exercise 7.22. Scott defines those systems but does not separately state the embeddings. Challenge.lean fixes the…

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-24-000001
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-24-000001/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-24-000001/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'