Verified Program Extraction in Number Theory: The Fundamental Theorem of Arithmetic and Relatives
Fuente:
arXiv
Guardado en:
| Autor principal: | |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866913155900243968 |
|---|---|
| author | Wiesnet, Franziskus |
| author_facet | Wiesnet, Franziskus |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_03460 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Verified Program Extraction in Number Theory: The Fundamental Theorem of Arithmetic and Relatives Wiesnet, Franziskus Logic 68V20 (Primary) 03F10, 03B35, 11Y05, 11Y16, 11A51 (Secondary) F.4.1 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. |
| title | Verified Program Extraction in Number Theory: The Fundamental Theorem of Arithmetic and Relatives |
| topic | Logic 68V20 (Primary) 03F10, 03B35, 11Y05, 11Y16, 11A51 (Secondary) F.4.1 |
| url | https://arxiv.org/abs/2504.03460 |