Abstract:We describe a Lean 4 formalization of the algorithms and domain types from NYU Computer Science Technical Report \#232, \emph{An ICON Package for Experimenting with Euclidean Domains} (Ericson, 1986). The original system implemented Lipson's catalog of procedures over integers, rationals, modular rings, polynomial rings, and truncated power series via a custom runtime dispatch mechanism in Icon. The present work separates three concerns: mathematical definitions grounded in Mathlib's \texttt{EuclideanDomain} hierarchy, computable mirrors suitable for evaluation and regression testing, and report-formatting infrastructure that reproduces the 1986 benchmark output line-for-line. All fourteen application algorithms from Section 3 of the report are defined and typecheck without \texttt{sorry}; those grounded in Mathlib -- chiefly integer gcd and extended Euclid -- additionally carry machine-checked proofs. We classify each procedure by its epistemic status relative to Mathlib, enumerate the coherence obligations between the proof and computable layers, and state precisely what is theorem-backed versus regression-trusted. The formalization makes explicit the verification boundary that the 1986 package crossed only informally.
From: Lars Ericson [view email]
[v1]
Sun, 14 Jun 2026 00:32:47 UTC (11 KB)
此内容由惯性聚合(RSS阅读器)自动聚合整理，仅供阅读参考。 原文来自 — 版权归原作者所有。