Verified Program Extraction in Number Theory: The Fundamental Theorem of Arithmetic and Relatives
Franziskus Wiesnet
TL;DR
The paper demonstrates how to formalize elementary number theory in the Minlog proof assistant and to extract verified, executable algorithms in Haskell. It foregrounds the computational content of proofs, comparing unary natural-number representations with binary positive-number encodings, and shows how choices impact performance in core tasks like gcd, primality, and prime-factorization. Key contributions include formalized existence and uniqueness of prime factorization, Bézout-type constructions without negative numbers, and explicit extracted terms for gcd, prime-factorization, and Fermat’s factorization. The work bridges formal verification and practical computation, providing a pathway toward verified computer algebra systems and refined connections between formal proofs and traditional textbook reasoning.
Abstract
This article revisits standard theorems from elementary number theory through a constructive, algorithmic, and proof-theoretic perspective, within the theory of computable functionals. Key examples include Bézout's identity, the fundamental theorem of arithmetic, and Fermat's factorization method. All definitions and theorems are fully formalized in the proof assistant Minlog, laying the foundation for a comprehensive formal framework for number theory within Minlog. While formalization guarantees correctness, the primary emphasis is on the computational content of proofs. Leveraging Minlog's built-in program extraction, we obtain executable terms that are exported as Haskell code. The efficiency of the extracted programs plays a central role. We show how performance considerations influence even the initial formulation of theorems and proofs. In particular, we compare formalizations 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 formalization in contrast to informal reasoning. The complete formalization is available online and linked for reference. Minlog's tactic scripts are designed to follow the structure of natural-language proofs, allowing each derivation step to be traced precisely and thus bridging the gap between formal and classical mathematical reasoning.