pith. sign in

arxiv: 2504.03460 · v5 · pith:VXLT3AT7new · submitted 2025-04-04 · 🧮 math.LO

Verified Program Extraction in Number Theory: The Fundamental Theorem of Arithmetic and Relatives

Franziskus Wiesnet This is my paper

Pith reviewed 2026-05-25 07:59 UTC · model grok-4.3

classification 🧮 math.LO
keywords Minlogprogram extractionfundamental theorem of arithmeticBézout's identityFermat factorizationconstructive mathematicsformal verificationHaskell code
0
0 comments X

The pith

Theorems from elementary number theory are fully formalized in Minlog with proofs yielding extracted executable Haskell code.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper revisits standard results such as Bézout's identity, the fundamental theorem of arithmetic, and Fermat's factorization method from a constructive viewpoint inside the theory of computable functionals. All definitions and theorems receive complete formalization inside the Minlog proof assistant, after which the system's program extraction produces executable terms that are exported as Haskell programs. The work stresses that efficiency of the resulting code shapes the original choice of proof formulations, especially the decision between binary and unary encodings of natural numbers. A reader would care because the approach turns mathematical proofs directly into verified, runnable code while keeping every derivation step traceable through tactic scripts that mirror ordinary reasoning.

Core claim

Within the theory of computable functionals TCF, the paper formalizes Bézout's identity, the fundamental theorem of arithmetic, and Fermat's factorization method inside Minlog. Program extraction turns these formal proofs into executable terms that are then exported as Haskell code. Efficiency considerations affect the choice of formulations, leading to explicit comparisons between binary and unary representations of natural numbers. The complete formalization, including tactic scripts that follow the structure of natural-language proofs, is available online.

What carries the argument

Minlog's built-in program extraction from proofs formalised in the theory of computable functionals TCF.

If this is right

  • The extracted Haskell programs implement verified versions of Bézout's identity and the fundamental theorem of arithmetic.
  • Binary encodings of natural numbers produce more efficient extracted code than unary encodings for the same theorems.
  • Performance requirements can be incorporated into the original statement and proof of a theorem to improve the extracted program.
  • Tactic scripts that mirror natural-language proofs allow each formal step to be traced back to its informal counterpart.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The extracted code could be integrated into larger certified computational number-theory libraries.
  • The same extraction workflow might be applied to theorems beyond elementary number theory inside the Minlog environment.
  • Direct comparison of extraction speed and code size across different proof assistants would quantify the practical impact of the Minlog approach.

Load-bearing premise

The formalization in Minlog correctly captures the intended mathematical content and the extraction mechanism produces Haskell code whose runtime behavior matches the proofs.

What would settle it

Executing the extracted Haskell program for the fundamental theorem of arithmetic on a composite integer whose prime factorization is independently known and obtaining an incorrect factorization list would show that the extraction failed to preserve the proof's content.

read the original abstract

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\'ezout'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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 3 minor

Summary. The paper claims to have fully formalized several standard theorems from elementary number theory—including Bézout's identity, the fundamental theorem of arithmetic, and Fermat's factorization method—inside the Minlog proof assistant under the theory of computable functionals TCF. It extracts executable Haskell programs from the proofs via Minlog's built-in mechanism, compares the efficiency of binary versus unary encodings of the naturals, and makes the complete tactic scripts and formalization available online. The work stresses computational content and how performance considerations shape the choice of formulations and proofs.

Significance. If the formalizations hold, the paper supplies machine-checked proofs together with reproducible extracted code for core number-theoretic results, establishing an initial constructive framework for number theory inside Minlog. The explicit availability of the full tactic scripts and the focus on efficiency trade-offs between representations constitute concrete strengths that support reproducibility and further development in verified program extraction.

minor comments (3)
  1. The abstract states that 'several core proofs' are presented in detail, yet the manuscript would benefit from explicit section headings or a table that maps each theorem to its corresponding Minlog script file and extracted term, improving traceability for readers.
  2. Notation for the two number representations (binary vs. unary) is introduced but not consistently contrasted in the text; a short comparative table of the extracted terms or their complexity would clarify the performance claims without requiring the reader to consult the external repository.
  3. The manuscript refers to 'the complete formalisation' being available online; adding a brief appendix that reproduces the top-level theorem statements and extraction commands (even if the full scripts remain external) would make the central claims more self-contained.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary of the manuscript, recognition of its strengths in reproducibility and efficiency comparisons, and recommendation of minor revision. No specific major comments appear in the report, so we have no individual points requiring point-by-point rebuttal or revision.

Circularity Check

0 steps flagged

No significant circularity; formalization is externally verified

full rationale

The paper formalizes standard constructive number theory results (Bézout, FTA, Fermat factorization) inside the external proof assistant Minlog and extracts Haskell code via Minlog's documented extraction mechanism. No equations, parameters, or predictions are present. No self-citations are used to justify load-bearing steps; the manuscript explicitly states that the full tactic scripts and formalization are available online for independent checking. The central claim reduces to the correctness of Minlog's type system and extraction, which are external to the paper and machine-checked. This matches the default expectation of a non-circular formalization paper.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper relies on the pre-existing theory of computable functionals TCF and the Minlog system; no new free parameters, ad-hoc axioms, or invented entities are introduced.

axioms (1)
  • domain assumption Theory of computable functionals (TCF)
    The work is explicitly framed within TCF as stated in the abstract.

pith-pipeline@v0.9.0 · 5749 in / 1298 out tokens · 48210 ms · 2026-05-25T07:59:43.052083+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

90 extracted references · 90 canonical work pages · 1 internal anchor

  1. [1]

    Ziegler.Das BUCH der Beweise

    Martin Aigner and Günter M. Ziegler.Das BUCH der Beweise. Springer Berlin Heidelberg,

    work page

  2. [2]

    Auflage.doi:10.1007/978-3-642-02259-3

    3. Auflage.doi:10.1007/978-3-642-02259-3

    work page doi:10.1007/978-3-642-02259-3

  3. [3]

    Intrinsically Correct Algorithms and Recursive Coalgebras

    Cass Alexandru, Henning Urbat, and Thorsten Wißmann. Intrinsically Correct Algorithms and Recursive Coalgebras. December 2025.arXiv:2512.10748, doi:10.48550/ARXIV.251 2.10748

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.251 2025

  4. [4]

    Extending Stein’s GCD algorithm and a comparison to Euclid’s GCD algorithm, 2019

    Joris Barkema. Extending Stein’s GCD algorithm and a comparison to Euclid’s GCD algorithm, 2019. Bachelor’s Thesis. URL:https://studenttheses.uu.nl/handle/20.50 0.12932/33194

    work page 2019

  5. [5]

    Formal Correctness Proofs of Functional Pro- grams: Dijkstra’s Algorithm, a Case Study

    Holger Benl and Helmut Schwichtenberg. Formal Correctness Proofs of Functional Pro- grams: Dijkstra’s Algorithm, a Case Study. In U. Berger and H. Schwichtenberg, editors, Computational Logic, volume 165 ofSeries F: Computer and Systems Sciences, pages 113–

    work page

  6. [6]

    doi:10.1007/978-3-642-58622-4_4

    Proceedings of the NATO Advanced Study Institute on Computational Logic, held in Marktoberdorf, Germany, July 29 – August 10, 1997, Springer Berlin Heidelberg, 1999. doi:10.1007/978-3-642-58622-4_4

    work page doi:10.1007/978-3-642-58622-4_4 1997

  7. [7]

    Program Extraction from Normalization Proofs.Studia Logica, 82(1):25–49, February 2006.doi: 10.1007/s11225-006-6604-5

    Ulrich Berger, Stefan Berghofer, Pierre Letouzey, and Helmut Schwichtenberg. Program Extraction from Normalization Proofs.Studia Logica, 82(1):25–49, February 2006.doi: 10.1007/s11225-006-6604-5

    work page doi:10.1007/s11225-006-6604-5 2006

  8. [8]

    Refined program extraction from classical proofs.Annals of Pure and Applied Logic, 114(1–3):3–25, April 2002.doi: 10.1016/s0168-0072(01)00073-2

    Ulrich Berger, Wilfried Buchholz, and Helmut Schwichtenberg. Refined program extraction from classical proofs.Annals of Pure and Applied Logic, 114(1–3):3–25, April 2002.doi: 10.1016/s0168-0072(01)00073-2

    work page doi:10.1016/s0168-0072(01)00073-2 2002

  9. [9]

    Springer Berlin Heidelberg, 1998.doi:10.1007/3-540-49254-2_4

    Ulrich Berger, Matthias Eberl, and Helmut Schwichtenberg.Normalization by Evaluation, pages 117–137. Springer Berlin Heidelberg, 1998.doi:10.1007/3-540-49254-2_4

    work page doi:10.1007/3-540-49254-2_4 1998

  10. [10]

    Springer Berlin Heidelberg, 2011

    Ulrich Berger, Kenji Miyamoto, Helmut Schwichtenberg, and Monika Seisenberger.Minlog - A Tool for Program Extraction Supporting Algebras and Coalgebras, pages 393–399. Springer Berlin Heidelberg, 2011. 4th International Conference, CALCO 2011, Winchester, UK, August 30 – September 2, 2011. Proceedings.doi:10.1007/978-3-642-22944-2_29

    work page doi:10.1007/978-3-642-22944-2_29 2011

  11. [11]

    Logic for Gray-code Computation

    Ulrich Berger, Kenji Miyamoto, Helmut Schwichtenberg, and Hideki Tsuiki. Logic for Gray-code Computation. In D. Probst and P. Schuster, editors,Concepts of Proof in Mathematics, Philosophy, and Computer Science, pages 69–110. De Gruyter, July 2016. doi:10.1515/9781501502620-005

    work page doi:10.1515/9781501502620-005 2016

  12. [12]

    The greatest common divisor: A case study for program extraction from classical proofs

    Ulrich Berger and Helmut Schwichtenberg. The greatest common divisor: A case study for program extraction from classical proofs. In Stefano Berardi and Mario Coppo, editors, Types for Proofs and Programs, volume 1158, pages 36–46. Springer Berlin Heidelberg,

    work page

  13. [13]

    doi:10.1007/3-540-61780-9_60

    International Workshop, TYPES ’95 Torino, Italy, June 5–8, 1995 Selected Papers. doi:10.1007/3-540-61780-9_60

    work page doi:10.1007/3-540-61780-9_60 1995

  14. [14]

    Number 51 in Other titles in applied mathematics

    Ake Björck.Numerical methods for least squares problems. Number 51 in Other titles in applied mathematics. Society for Industrial and Applied Mathematics, Philadelphia, 1996. 47

    work page 1996

  15. [15]

    Formal and Efficient Primality Proofs by Use of Computer Algebra Oracles.Journal of Symbolic Computation, 32(1–2):55–70, July 2001

    Olga Caprotti and Martijn Oostdijk. Formal and Efficient Primality Proofs by Use of Computer Algebra Oracles.Journal of Symbolic Computation, 32(1–2):55–70, July 2001. doi:10.1006/jsco.2001.0457

    work page doi:10.1006/jsco.2001.0457 2001

  16. [16]

    The Lattice of Natural Numbers and The Sublattice of it.The Set of Prime Numbers.Journal of Formalized Mathematics, 1991

    Marek Chmur. The Lattice of Natural Numbers and The Sublattice of it.The Set of Prime Numbers.Journal of Formalized Mathematics, 1991. Related file: https://miza r.uwb.edu.pl/version/current/mml/newton.miz .Accessed 2026-01-21. URL: https: //mizar.uwb.edu.pl/JFM/pdf/nat_lat.pdf

    work page 1991

  17. [17]

    Number 138 in Graduate texts in mathematics

    Henri Cohen.A course in computational algebraic number theory. Number 138 in Graduate texts in mathematics. Springer Berlin Heidelberg, Berlin, 1993.doi:10.1007/978-3-662-0 2945-9

    work page doi:10.1007/978-3-662-0 1993

  18. [18]

    Springer-Verlag, 2 edition, 2005.doi:10.1007/0-387-28979-8

    Richard Crandall and Carl Pomerance.Prime Numbers: A Computational Perspective. Springer-Verlag, 2 edition, 2005.doi:10.1007/0-387-28979-8

    work page doi:10.1007/0-387-28979-8 2005

  19. [19]

    Springer International Publishing, 2021.doi:10.1007/978-3-030-79876-5_36

    Adrian De Lon, Peter Koepke, Anton Lorenzen, Adrian Marti, Marcel Schütz, and Makarius Wenzel.The Isabelle/Naproche Natural Language Proof Assistant, pages 614–624. Springer International Publishing, 2021.doi:10.1007/978-3-030-79876-5_36

    work page doi:10.1007/978-3-030-79876-5_36 2021

  20. [20]

    Theory Euclidean_Algorithm, 2025

    Manuel Eberl. Theory Euclidean_Algorithm, 2025. Accessed 2026-01-20. URL:https: //isabelle.in.tum.de/library/HOL/HOL-Computational_Algebra/Euclidean_Algorit hm.html

    work page 2025

  21. [21]

    Springer Fachmedien Wiesbaden, 2015.doi: 10.1007/978-3-658-06540-9

    Otto Forster.Algorithmische Zahlentheorie. Springer Fachmedien Wiesbaden, 2015.doi: 10.1007/978-3-658-06540-9

    work page doi:10.1007/978-3-658-06540-9 2015

  22. [22]

    Otto Forster. Aribas. Website, 2024. Accessed: 2025-03-07. URL:https://www.mathemat ik.uni-muenchen.de/~forster/sw/aribas.html

    work page 2024

  23. [23]

    GNU MP Manual (version 6.3.0): Multiplication Algorithms

    Free Software Foundation, Inc. GNU MP Manual (version 6.3.0): Multiplication Algorithms. https://gmplib.org/manual/Multiplication-Algorithms.html , 2020. Accessed 2026-02-01

    work page 2020

  24. [24]

    Karádais, and Helmut Schwichtenberg

    Simon Huber, Basil A. Karádais, and Helmut Schwichtenberg. Towards a Formal Theory of Computability. In R. Schindler, editor,Ways of Proof Theory: Festschrift for W. Pohlers, pages 257–282. De Gruyter, December 2010.doi:10.1515/9783110324907.257

    work page doi:10.1515/9783110324907.257 2010

  25. [25]

    Verification of the Miller–Rabin probabilistic primality test.The Journal of Logic and Algebraic Programming, 56(1–2):3–21, May 2003.doi:10.1016/s1567-8326(02)00065 -6

    Joe Hurd. Verification of the Miller–Rabin probabilistic primality test.The Journal of Logic and Algebraic Programming, 56(1–2):3–21, May 2003.doi:10.1016/s1567-8326(02)00065 -6

    work page doi:10.1016/s1567-8326(02)00065 2003

  26. [26]

    Embedding classical in minimal implicational logic.Mathematical Logic Quarterly, 62(1–2):94–101, January 2016.doi:10.1002/malq.2 01400099

    Hajime Ishihara and Helmut Schwichtenberg. Embedding classical in minimal implicational logic.Mathematical Logic Quarterly, 62(1–2):94–101, January 2016.doi:10.1002/malq.2 01400099

    work page doi:10.1002/malq.2 2016

  27. [27]

    Karádais.Towards an Arithmetic for Partial Computable Functionals

    Basil A. Karádais.Towards an Arithmetic for Partial Computable Functionals. PhD thesis, Ludwig-Maximilians University Munich, 2013

    work page 2013

  28. [28]

    Formalizing and Autoformalizing Euclid’s Lemma in Naproche

    Peter Koepke. Formalizing and Autoformalizing Euclid’s Lemma in Naproche. Slides: https://github.com/naproche/Talks/blob/master/2025/koepke_formalizing-and-a utoformalizing-euclids-lemma-in-naproche.pdf, 2025. Talk at theNatFoMworkshop atCICM 2025, Brasília, Brazil, ccessed 2026-01-27

    work page 2025

  29. [29]

    100 Theorems

    Peter Koepke, Mateusz Marcol, and Patrick Schäfer. Formalizing Sets and Numbers, and some of Wiedijk’s “100 Theorems” in Naproche. Online PDF, 2023. Accessed 2026-01-19. URL:https://naproche.github.io/100_theorems.ftl.pdf. 48

    work page 2023

  30. [30]

    Springer Monographs in Mathematics

    Ulrich Kohlenbach.Applied Proof Theory: Proof Interpretations and their Use in Mathematics. Springer Monographs in Mathematics. Springer Berlin Heidelberg, 2008. doi:10.1007/978-3-540-77533-1

    work page doi:10.1007/978-3-540-77533-1 2008

  31. [31]

    Fundamental Theorem of Arithmetic.Formalized Mathematics, 12(2):179–186, 2004

    Artur Korniłowicz and Piotr Rudnicki. Fundamental Theorem of Arithmetic.Formalized Mathematics, 12(2):179–186, 2004. URL:https://mizar.uwb.edu.pl/fm/2004-12/pdf1 2-2/nat_3.pdf

    work page 2004

  32. [32]

    Interpretation of Analysis by Means of Constructive Functionals of Finite Types

    Georg Kreisel. Interpretation of Analysis by Means of Constructive Functionals of Finite Types. In A. Heyting, editor,Constructivity in mathematics, pages 101–128. North-Holland Pub. Co., 1959

    work page 1959

  33. [33]

    Lookahead analysis in exact real arithmetic with logical methods.Theoretical Computer Science, 943:171–186, January 2023.doi:10.1016/ j.tcs.2022.10.003

    Nils Köpp and Helmut Schwichtenberg. Lookahead analysis in exact real arithmetic with logical methods.Theoretical Computer Science, 943:171–186, January 2023.doi:10.1016/ j.tcs.2022.10.003

    work page 2023

  34. [34]

    Using information systems to solve recursive domain equations.Information and Computation, 91(2):232–258, April 1991.doi:10.1016/ 0890-5401(91)90068-d

    Kim Guldstrand Larsen and Glynn Winskel. Using information systems to solve recursive domain equations.Information and Computation, 91(2):232–258, April 1991.doi:10.1016/ 0890-5401(91)90068-d

    work page 1991

  35. [35]

    Library mathcomp.ssreflect.prime, 2020

    Mathematical Components Development Team. Library mathcomp.ssreflect.prime, 2020. Released 26 Nov 2020. Accessed 2026-01-21. URL:https://math-comp.github.io/html doc_1_12_0/mathcomp.ssreflect.prime.html

    work page 2020

  36. [36]

    Mathlib.Data.Int.GCD, 2026

    Mathlib Community. Mathlib.Data.Int.GCD, 2026. Accessed 2026-01-21. URL:https:// leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Factors.html

    work page 2026

  37. [37]

    Mathlib.Data.Nat.Factors, 2026

    Mathlib Community. Mathlib.Data.Nat.Factors, 2026. Accessed 2026-01-21. URL:https: //leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Int/GCD.html

    work page 2026

  38. [38]

    Mathlib.Data.Nat.Prime.Defs, 2026

    Mathlib Community. Mathlib.Data.Nat.Prime.Defs, 2026. Accessed 2026-01-21. URL: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Prime/ Defs.html

    work page 2026

  39. [39]

    Mathlib.Data.Nat.Prime.Infinite, 2026

    Mathlib Community. Mathlib.Data.Nat.Prime.Infinite, 2026. Accessed 2026-01-21. URL: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Prime/ Infinite.html

    work page 2026

  40. [40]

    Menezes, Paul C

    Alfred J. Menezes, Paul C. van Oorschot, and Scott A. Vanstone.Handbook of Applied Cryptography. CRC Press, December 2018.doi:10.1201/9780429466335

    work page doi:10.1201/9780429466335 2018

  41. [41]

    Smith, Mateusz Paprocki, Ondrej Certik, Sergey B

    Aaron Meurer, Christopher P. Smith, Mateusz Paprocki, Ondrej Certik, Sergey B. Kirpichev, Matthew Rocklin, AMiT Kumar, Sergiu Ivanov, Jason K. Moore, Sartaj Singh, Thilina Rathnayake, Sean Vig, Brian E. Granger, Richard P. Muller, Francesco Bonazzi, Harsh Gupta, Shivam Vats, Fredrik Johansson, Fabian Pedregosa, Matthew J. Curry, Andy R. Terrel, Stepan Rou...

    work page doi:10.7717/peerj-cs.103 2017

  42. [42]

    Gary L. Miller. Riemann’s Hypothesis and tests for primality. InProceedings of seventh annual ACM symposium on Theory of computing, STOC ’75, pages 234–239. ACM Press, 1975.doi:10.1145/800116.803773

    work page doi:10.1145/800116.803773 1975

  43. [43]

    PhD thesis, Ludwig-Maximilians University Munich, 2013

    Kenji Miyamoto.Program extraction from coinductive proofs and its application to exact real arithmetic. PhD thesis, Ludwig-Maximilians University Munich, 2013. 49

    work page 2013

  44. [44]

    The Minlog System.https://www.mathematik.uni-muenchen.de/~log ik/minlog/, 2026

    Kenji Miyamoto. The Minlog System.https://www.mathematik.uni-muenchen.de/~log ik/minlog/, 2026. Accessed 2026-02-10. URL:https://www.mathematik.uni-muenchen. de/~logik/minlog/

    work page 2026

  45. [45]

    Program Extrac- tion from Nested Definitions

    Kenji Miyamoto, Fredrik Nordvall Forsberg, and Helmut Schwichtenberg. Program Extrac- tion from Nested Definitions. In S. Blazy, C. Paulin-Mohring, and D. Pichardie, editors, Interactive Theorem Proving, volume 7998 ofLNCS, pages 370–385. Springer Berlin Hei- delberg, 2013. 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedi...

    work page doi:10.1007/978-3-642-39634-2_27 2013

  46. [46]

    Program extraction in exact real arithmetic

    Kenji Miyamoto and Helmut Schwichtenberg. Program extraction in exact real arithmetic. Mathematical Structures in Computer Science, 25(8):1692–1704, November 2014.doi: 10.1017/s0960129513000327

    work page doi:10.1017/s0960129513000327 2014

  47. [47]

    Vieweg+Teubner, 2011.doi:10.1007/978-3-8348-8263-9

    Stefan Müller-Stach and Jens Piontkowski.Elementare und algebraische Zahlentheorie. Vieweg+Teubner, 2011.doi:10.1007/978-3-8348-8263-9

    work page doi:10.1007/978-3-8348-8263-9 2011

  48. [48]

    Extended Euclidean Algorithm and CRT Algorithm.Formalized Mathematics, 20(2):175–179, December 2012.doi:10.2478/v1 0037-012-0020-2

    Hiroyuki Okazaki, Yosiki Aoki, and Yasunari Shidama. Extended Euclidean Algorithm and CRT Algorithm.Formalized Mathematics, 20(2):175–179, December 2012.doi:10.2478/v1 0037-012-0020-2

    work page doi:10.2478/v1 2012

  49. [49]

    Lawrence C. Paulson. Verifying the binary algorithm for greatest common divisors, 2023. Accessed 2026-01-20. URL:https://lawrencecpaulson.github.io/2023/02/22/Binary _GCD.html

    work page 2023

  50. [50]

    A Brief History of Natural Deduction.History and Philosophy of Logic, 20(1):1–31, January 1999.doi:10.1080/014453499298165

    Francis Jeffry Pelletier. A Brief History of Natural Deduction.History and Philosophy of Logic, 20(1):1–31, January 1999.doi:10.1080/014453499298165

    work page doi:10.1080/014453499298165 1999

  51. [51]

    Advances in the Theory of ComputableFunctionals TCF+ due to its Im- plementation, 2013

    Iosif Petrakis. Advances in the Theory of ComputableFunctionals TCF+ due to its Im- plementation, 2013. online: https://www.math.lmu.de/~petrakis/TCF+.pdf . URL: https://www.math.lmu.de/~petrakis/TCF+.pdf

    work page 2013

  52. [52]

    PhD thesis, Stanford University, 1966

    Richard Alan Platek.Foundations of recursion theory. PhD thesis, Stanford University, 1966

    work page 1966

  53. [53]

    Analysis and Comparison of Some Integer Factoring Algorithms

    Carl Pomerance. Analysis and Comparison of Some Integer Factoring Algorithms. In Jr. H.W. Lenstra and R. Tijdeman, editors,Computational Methods in Number Theory, pages 89–139. Math. Centrum, Amsterdam, 1982

    work page 1982

  54. [54]

    @Dover books on mathematics

    Dag Prawitz.Natural deduction: A proof-theoretical study. @Dover books on mathematics. Courier Dover Publications, Mineola, N.Y, 2006. Includes bibliographical references (p. [106]-109) and indexes

    work page 2006

  55. [55]

    Elementary Number Theory Problems

    Karol Pąk. Elementary Number Theory Problems. Part XVI.Formalized Mathematics, 32(1):203–212, August 2024.doi:10.2478/forma-2024-0017

    work page doi:10.2478/forma-2024-0017 2024

  56. [56]

    Michael O. Rabin. Probabilistic algorithm for testing primality.Journal of Number Theory, 12(1):128–138, February 1980.doi:10.1016/0022-314x(80)90084-0

    work page doi:10.1016/0022-314x(80)90084-0 1980

  57. [57]

    The agda-unimath library, 2026

    Egbert Rijke, Fredrik Bakke, and Vojtěch Štěpančík. The agda-unimath library, 2026. URL: https://unimath.github.io/agda-unimath/

    work page 2026

  58. [58]

    Library Stdlib.PArith.BinPosDef,

    Rocq Prover Developers and Coq/Stdlib Contributors. Library Stdlib.PArith.BinPosDef,

    work page

  59. [59]

    URL: https://rocq-prover.org/doc/V9.1.0/stdlib/Stdl ib.ZArith.Znumtheory.html

    Accessed 2026-01-21. URL: https://rocq-prover.org/doc/V9.1.0/stdlib/Stdl ib.ZArith.Znumtheory.html. 50

    work page 2026

  60. [60]

    Library Stdlib.ZArith.Znumtheory,

    Rocq Prover Developers and Coq/Stdlib Contributors. Library Stdlib.ZArith.Znumtheory,

    work page

  61. [61]

    URL: https://rocq-prover.org/doc/v9.0/stdlib/Stdlib .PArith.BinPosDef.html

    Accessed 2026-01-21. URL: https://rocq-prover.org/doc/v9.0/stdlib/Stdlib .PArith.BinPosDef.html

    work page 2026

  62. [62]

    Primitive Recursion on the Partial Continuous Functionals

    Helmut Schwichtenberg. Primitive Recursion on the Partial Continuous Functionals. In M. Broy, editor,Informatik und Mathematik, pages 251–268. Springer Berlin Heidelberg, 1991.doi:10.1007/978-3-642-76677-0_18

    work page doi:10.1007/978-3-642-76677-0_18 1991

  63. [63]

    Proofs as Programs

    Helmut Schwichtenberg. Proofs as Programs. In P. Aczel, H. Simmons, and S. Wainer, editors, Proof Theory: A selection of papers from the Leeds Proof Theory Programme 1990, page 79–114, Cambridge, 1993. Cambridge University Press. Title from publisher’s bibliographic system (viewed on 24 Feb 2016).doi:10.1017/CBO9780511896262.005

    work page doi:10.1017/cbo9780511896262.005 1990

  64. [64]

    Helmut Schwichtenberg. Minlog. In Freek Wiedijk, editor,The Seventeen Provers of the World, volume 3600, pages 151–157. Springer Berlin Heidelberg, 2006.doi:10.1007/1154 2384_19

    work page doi:10.1007/1154 2006

  65. [65]

    Program Extraction from Proofs: The Fan Theorem for Uniformly Coconvex Bars

    Helmut Schwichtenberg. Program Extraction from Proofs: The Fan Theorem for Uniformly Coconvex Bars. In S. Centrone, S. Negri, D. Sarikaya, and P. Schuster, editors,Mathesis Universalis, Computability and Proof, volume 412 ofSynthese Library, pages 333–341. Springer International Publishing, 2019.doi:10.1007/978-3-030-20447-1_17

    work page doi:10.1007/978-3-030-20447-1_17 2019

  66. [66]

    Cambridge University Press, April 2023.doi:10.1017/9781009039888.027

    Helmut Schwichtenberg.Computational Aspects of Bishop’s Constructive Mathematics, pages 715–748. Cambridge University Press, April 2023.doi:10.1017/9781009039888.027

    work page doi:10.1017/9781009039888.027 2023

  67. [67]

    Logic for Exact Real Arithmetic: Multiplication

    Helmut Schwichtenberg. Logic for Exact Real Arithmetic: Multiplication. InMathematics for Computation (M4C), chapter 3, pages 39–69. World Scientific, April 2023.doi:10.114 2/9789811245220_0003

    work page 2023

  68. [68]

    Logic II: proofs and programs, July 2025

    Helmut Schwichtenberg. Logic II: proofs and programs, July 2025. Lecture notes, summer term 2025. URL: https://www.mathematik.uni-muenchen.de/~schwicht/lectures/log ic/ss25/tcf.pdf

    work page 2025

  69. [69]

    Higman’s Lemma and its Computational Content

    Helmut Schwichtenberg, Monika Seisenberger, and Franziskus Wiesnet. Higman’s Lemma and its Computational Content. In R. Kahle, T. Strahm, and T. Studer, editors,Advances in Proof Theory, pages 353–375. Springer International Publishing, 2016.doi:10.1007/97 8-3-319-29198-7_11

    work page doi:10.1007/97 2016

  70. [70]

    Minimal from classical proofs.Annals of Pure and Applied Logic, 164(6):740–748, June 2013.doi:10.1016/j.apal.2012.05.009

    Helmut Schwichtenberg and Christoph Senjak. Minimal from classical proofs.Annals of Pure and Applied Logic, 164(6):740–748, June 2013.doi:10.1016/j.apal.2012.05.009

    work page doi:10.1016/j.apal.2012.05.009 2013

  71. [71]

    Wainer.Proofs and Computations

    Helmut Schwichtenberg and Stanley S. Wainer.Proofs and Computations. Perspectives in Logic. Cambridge University Press, December 2012.doi:10.1017/cbo9781139031905

    work page doi:10.1017/cbo9781139031905 2012

  72. [72]

    Helmut Schwichtenberg and Stanley S. Wainer. Tiered Arithmetics. In G. Jäger and W. Sieg, editors,Feferman on Foundations, volume 13, pages 145–168. Springer International Publishing, 2017.doi:10.1007/978-3-319-63334-3_6

    work page doi:10.1007/978-3-319-63334-3_6 2017

  73. [73]

    Logic for exact real arithmetic.Logical Methods in Computer Science, 17(2):7:1–7:27, April 2021.doi:10.23638/LMCS-17(2: 7)2021

    Helmut Schwichtenberg and Franziskus Wiesnet. Logic for exact real arithmetic.Logical Methods in Computer Science, 17(2):7:1–7:27, April 2021.doi:10.23638/LMCS-17(2: 7)2021

    work page doi:10.23638/lmcs-17(2: 2021

  74. [74]

    Scott.Domains for denotational semantics, pages 577–610

    Dana S. Scott.Domains for denotational semantics, pages 577–610. Springer Berlin Heidelberg, 1982.doi:10.1007/bfb0012801. 51

    work page doi:10.1007/bfb0012801 1982

  75. [75]

    Dana S. Scott. A type-theoretical alternative to ISWIM, CUCH, OWHY.Theoretical Computer Science, 121(1):411–440, 1993. URL:https://www.sciencedirect.com/scienc e/article/pii/030439759390095B,doi:10.1016/0304-3975(93)90095-B

    work page doi:10.1016/0304-3975(93)90095-b 1993

  76. [76]

    Computational problems associated with Racah algebra.Journal of Computa- tional Physics, 1(3):397–405, February 1967.doi:10.1016/0021-9991(67)90047-2

    Josef Stein. Computational problems associated with Racah algebra.Journal of Computa- tional Physics, 1(3):397–405, February 1967.doi:10.1016/0021-9991(67)90047-2

    work page doi:10.1016/0021-9991(67)90047-2 1967

  77. [77]

    Theory Primes, 2025

    Christophe Tabacznyj, Lawrence Paulson, Amine Chaieb, Thomas Rasmussen, Jeremy Avigad, Tobias Nipkow, and Manuel Eberl. Theory Primes, 2025. Accessed 2026-01-20. URL: https://isabelle.in.tum.de/library/HOL/HOL-Computational_Algebra/Prime s.html

    work page 2025

  78. [78]

    Paulson, Amine Chaieb, Thomas M

    Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb, Thomas M. Rasmussen, Jeremy Avigad, and Tobias Nipkow. Theory GCD, 2025. Accessed 2026-01-20. URL: https: //isabelle.in.tum.de/dist/library/HOL/HOL/GCD.html

    work page 2025

  79. [79]

    Springer Berlin Heidelberg, 2007.doi:10.1007/978-3-540-74591-4_24

    Laurent Théry and Guillaume Hanrot.Primality Proving with Elliptic Curves, pages 319–333. Springer Berlin Heidelberg, 2007.doi:10.1007/978-3-540-74591-4_24

    work page doi:10.1007/978-3-540-74591-4_24 2007

  80. [80]

    Springer Berlin Heidelberg, 1973.doi:10.1007/bfb0066739

    Anne Sjerp Troelstra, editor.Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. Springer Berlin Heidelberg, 1973.doi:10.1007/bfb0066739

    work page doi:10.1007/bfb0066739 1973

Showing first 80 references.