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.

翻译：本文描述了对纽约大学计算机科学第232号技术报告《一个用于欧几里得域实验的ICON软件包》（Ericson，1986）中算法与域类型的Lean 4形式化实现。原系统通过Icon中自定义运行时调度机制实现了Lipson关于整数、有理数、模环、多项式环及截断幂级数的程序目录。当前工作将三个关注点分离：基于Mathlib的\texttt{EuclideanDomain}层次结构的数学定义、适用于求值与回归测试的可计算镜像、以及逐行复现1986年基准测试输出的报告格式化基础设施。报告第3节全部十四个应用算法均已定义并通过类型检查（不含\texttt{sorry}）；其中基于Mathlib的算法（主要是整数最大公约数与扩展欧几里得算法）额外附有机验证明。我们依据每个过程相对于Mathlib的认识论状态进行分类，列举证明层与可计算层之间的连贯性义务，并精确阐明哪些内容受定理支持、哪些受回归验证信任。该形式化明确揭示了1986年软件包仅以非正式方式跨越的验证边界。