We present a constructive treatment of central theorems from elementary number theory within the interactive proof system Minlog. Formalization in Minlog not only guarantees the correctness of the proofs but also enables the extraction of executable programs, with a particular focus on their computational content. For this purpose, we make use of Minlog’s built-in program extraction mechanism. To achieve efficient implementations, algorithmic aspects are already taken into account during the proof construction. For instance, the proofs explicitly use the binary representation of natural numbers, as it is significantly more efficient in computation than the traditional successor-based representation. The underlying Minlog implementation includes formalizations of theorems such as Bézout’s identity, the fundamental theorem of arithmetic, and Fermat’s factorization method. Using selected examples, we illustrate how this constructive and algorithmically oriented approach influences the structure of the proofs and how it differs from classical standard proofs. We also demonstrate the extracted programs in Haskell. While prior knowledge of Minlog or the underlying logical theory is helpful, the talk is designed to be accessible without it. Only a basic understanding of elementary number theory will be necessary.