A Lean 4 Formalization of Euclidean Domain Algorithms from a 1986 Icon Experimentation Package

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 $\mathtt{\text{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 $\mathtt{\text{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.