We examine theorems of elementary number theory using a constructive, computational, and proof-theoretic approach. Key theorems include Euclid’s proof of the infinitude of prime numbers, Bézout’s identity, the Fundamental Theorem of Arithmetic, and Fermat’s factorization method. These theorems have been formalized within the proof assistant Minlog, providing rigorous formal verification. Minlog allows the extraction of executable Haskell programs from proofs, demonstrating their computational utility. The implementations can be found in the folder examples/arith of the Minlog directory. Currently these files are only available and functional in the dev branch of Minlog. We explore interesting and instructive aspects of the proofs, the implementation in Minlog, and the extracted Haskell term. Additionally, we will highlight the unique features and advantages of Minlog as a proof assistant, offering the audience a deeper insight into its capabilities. The main focus of the presentation will be on the Fundamental Theorem of Arithmetic and Fermat’s factorization method.