Formalizes Bézout's identity, FTA, and Fermat factorization in Minlog with program extraction to Haskell, comparing binary vs unary encodings for performance.
Formal and Efficient Primality Proofs by Use of Computer Algebra Oracles.Journal of Symbolic Computation, 32(1–2):55–70, July 2001
1 Pith paper cite this work. Polarity classification is still indexing.
1
Pith paper citing it
fields
math.LO 1years
2025 1verdicts
UNVERDICTED 1representative citing papers
citing papers explorer
-
Verified Program Extraction in Number Theory: The Fundamental Theorem of Arithmetic and Relatives
Formalizes Bézout's identity, FTA, and Fermat factorization in Minlog with program extraction to Haskell, comparing binary vs unary encodings for performance.