数论中的验证程序提取：算术基本定理及其相关
Verified Program Extraction in Number Theory: The Fundamental Theorem of Arithmetic and Relatives
AI总结：
本文在可计算泛函理论TCF框架下，从构造性、算法和证明论视角重新审视初等数论标准定理，通过Minlog证明助手形式化定义和定理，并利用程序提取生成可执行的Haskell代码，重点研究提取程序的效率及其对定理表述的影响。
摘要：
本文从构造性、算法和证明论视角重新审视初等数论中的标准定理，这些定理被置于可计算泛函理论TCF的框架内。关键例子包括贝祖恒等式、算术基本定理和费马因式分解法。所有定义和定理都在证明助手Minlog中完全形式化，为Minlog中数论的全面形式化框架奠定了基础。虽然形式化保证了正确性，但主要重点在于证明的计算内容。利用Minlog内置的程序提取，我们获得可执行项并将其导出为Haskell代码。提取程序的效率起着核心作用。我们展示了性能考虑如何甚至影响定理和证明的原始表述。特别地，我们比较了基于自然数二进制编码的形式化与使用传统一元（后继）表示的形式化。我们详细介绍了几个核心证明，并反思了形式化与非形式化推理相比所面临的挑战。完整的形式化内容可在网上获取并全程链接。Minlog的策略脚本旨在遵循自然语言证明的结构，使得每个推导步骤都能被精确追踪，从而弥合形式化与经典数学推理之间的差距。
英文摘要：
This article revisits standard theorems from elementary number theory from a constructive, algorithmic, and proof-theoretic perspective, framed within the theory of computable functionals TCF. Key examples include Bézout's identity, the fundamental theorem of arithmetic, and Fermat's factorisation method. All definitions and theorems are fully formalised in the proof assistant Minlog, laying the foundation for a comprehensive formal framework for number theory within Minlog. While formalisation guarantees correctness, the primary emphasis is on the computational content of proofs. Leveraging Minlog's built-in program extraction, we obtain executable terms and export them as Haskell code. The efficiency of the extracted programs plays a central role. We show how performance considerations influence even the original formulation of theorems and proofs. In particular, we compare formalisations based on binary encodings of natural numbers with those using the traditional unary (successor-based) representation. We present several core proofs in detail and reflect on the challenges that arise from formalisation in contrast to informal reasoning. The complete formalisation is available online and linked throughout. Minlog's tactic scripts are designed to follow the structure of natural-language proofs, allowing each derivation step to be traced precisely and thereby bridging the gap between formal and classical mathematical reasoning.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
