-
Verified Program Extraction in Number Theory: The Fundamental Theorem of Arithmetic and Relatives
Authors:
Franziskus Wiesnet
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 foundatio…
▽ More
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.
△ Less
Submitted 11 April, 2025; v1 submitted 4 April, 2025;
originally announced April 2025.
-
Material Interpretation and Constructive Analysis of Maximal Ideals in $\mathbb{Z}[X]$
Authors:
Franziskus Wiesnet
Abstract:
This article presents the concept of material interpretation as a method to transform classical proofs into constructive ones. Using the case study of maximal ideals in $\mathbb{Z}[X]$, it demonstrates how a classical implication $A \to B$ can be rephrased as a constructive disjunction $\neg A \vee B$, with $\neg A$ representing a strong form of negation. The approach is based on on Gödel's Dialec…
▽ More
This article presents the concept of material interpretation as a method to transform classical proofs into constructive ones. Using the case study of maximal ideals in $\mathbb{Z}[X]$, it demonstrates how a classical implication $A \to B$ can be rephrased as a constructive disjunction $\neg A \vee B$, with $\neg A$ representing a strong form of negation. The approach is based on on Gödel's Dialectica interpretation, the strong negation, and potentially Herbrand disjunctions. The classical proof that every maximal ideal in $\mathbb{Z}[X]$ contains a prime number is revisited, highlighting its reliance on non-constructive principles such as the law of excluded middle. A constructive proof is then developed, replacing abstract constructs with explicit case distinctions and direct computations in $\mathbb{Z}[X]$. This proof clarifies the logical structure and reveals computational content. The article discusses broader applications, such as Zariski's Lemma, Hilbert's Nullstellensatz, and the Universal Krull-Lindenbaum Lemma, with an emphasis on practical implementation using tools such as Python and proof assistants. The material interpretation offers a promising framework for bridging classical and constructive mathematics, enabling algorithmic implementations.
△ Less
Submitted 10 April, 2025; v1 submitted 25 March, 2025;
originally announced March 2025.
-
Rates of convergence for asymptotically weakly contractive mappings in normed spaces
Authors:
Thomas Powell,
Franziskus Wiesnet
Abstract:
We study Krasnoselskii-Mann style iterative algorithms for approximating fixpoints of asymptotically weakly contractive mappings, with a focus on providing generalised convergence proofs along with explicit rates of convergence. More specifically, we define a new notion of being asymptotically $ψ$-weakly contractive with modulus, and present a series of abstract convergence theorems which both gen…
▽ More
We study Krasnoselskii-Mann style iterative algorithms for approximating fixpoints of asymptotically weakly contractive mappings, with a focus on providing generalised convergence proofs along with explicit rates of convergence. More specifically, we define a new notion of being asymptotically $ψ$-weakly contractive with modulus, and present a series of abstract convergence theorems which both generalise and unify known results from the literature. Rates of convergence are formulated in terms of our modulus of contractivity, in conjunction with other moduli and functions which form quantitative analogues of additional assumptions that are required in each case. Our approach makes use of ideas from proof theory, in particular our emphasis on abstraction and on formulating our main results in a quantitative manner. As such, the paper can be seen as a contribution to the proof mining program.
△ Less
Submitted 29 April, 2021;
originally announced April 2021.
-
Limits of real numbers in the binary signed digit representation
Authors:
Franziskus Wiesnet,
Nils Köpp
Abstract:
We extract verified algorithms for exact real number computation from constructive proofs. To this end we use a coinductive representation of reals as streams of binary signed digits. The main objective of this paper is the formalisation of a constructive proof that real numbers are closed with respect to limits. All the proofs of the main theorem and the first application are implemented in the M…
▽ More
We extract verified algorithms for exact real number computation from constructive proofs. To this end we use a coinductive representation of reals as streams of binary signed digits. The main objective of this paper is the formalisation of a constructive proof that real numbers are closed with respect to limits. All the proofs of the main theorem and the first application are implemented in the Minlog proof system and the extracted terms are further translated into Haskell. We compare two approaches. The first approach is a direct proof. In the second approach we make use of the representation of reals by a Cauchy-sequence of rationals. Utilizing translations between the two represenation and using the completeness of the Cauchy-reals, the proof is very short. In both cases we use Minlog's program extraction mechanism to automatically extract a formally verified program that transforms a converging sequence of reals, i.e.~a sequence of streams of binary signed digits together with a modulus of convergence, into the binary signed digit representation of its limit. The correctness of the extracted terms follows directly from the soundness theorem of program extraction. As a first application we use the extracted algorithms together with Heron's method to construct an algorithm that computes square roots with respect to the binary signed digit representation. In a second application we use the convergence theorem to show that the signed digit representation of real numbers is closed under multiplication.
△ Less
Submitted 18 August, 2022; v1 submitted 29 March, 2021;
originally announced March 2021.
-
Logic for exact real arithmetic
Authors:
Helmut Schwichtenberg,
Franziskus Wiesnet
Abstract:
Continuing earlier work of the first author with U. Berger, K. Miyamoto and H. Tsuiki, it is shown how a division algorithm for real numbers given as a stream of signed digits can be extracted from an appropriate formal proof. The property of being a real number represented as a stream is formulated by means of coinductively defined predicates, and formal proofs involve coinduction. The proof assi…
▽ More
Continuing earlier work of the first author with U. Berger, K. Miyamoto and H. Tsuiki, it is shown how a division algorithm for real numbers given as a stream of signed digits can be extracted from an appropriate formal proof. The property of being a real number represented as a stream is formulated by means of coinductively defined predicates, and formal proofs involve coinduction. The proof assistant Minlog is used to generate the formal proofs and extract their computational content as terms of the underlying theory, a form of type theory for finite or infinite data. Some experiments with running the extracted term are described, after its translation to Haskell.
△ Less
Submitted 19 April, 2021; v1 submitted 29 April, 2019;
originally announced April 2019.
-
An algorithmic approach to the existence of ideal objects in commutative algebra
Authors:
Thomas Powell,
Peter M Schuster,
Franziskus Wiesnet
Abstract:
The existence of ideal objects, such as maximal ideals in nonzero rings, plays a crucial role in commutative algebra. These are typically justified using Zorn's lemma, and thus pose a challenge from a computational point of view. Giving a constructive meaning to ideal objects is a problem which dates back to Hilbert's program, and today is still a central theme in the area of dynamical algebra, wh…
▽ More
The existence of ideal objects, such as maximal ideals in nonzero rings, plays a crucial role in commutative algebra. These are typically justified using Zorn's lemma, and thus pose a challenge from a computational point of view. Giving a constructive meaning to ideal objects is a problem which dates back to Hilbert's program, and today is still a central theme in the area of dynamical algebra, which focuses on the elimination of ideal objects via syntactic methods. In this paper, we take an alternative approach based on Kreisel's no counterexample interpretation and sequential algorithms. We first give a computational interpretation to an abstract maximality principle in the countable setting via an intuitive, state based algorithm. We then carry out a concrete case study, in which we give an algorithmic account of the result that in any commutative ring, the intersection of all prime ideals is contained in its nilradical.
△ Less
Submitted 7 March, 2019;
originally announced March 2019.
-
Limits with Signed Digit Streams
Authors:
Franziskus Wiesnet
Abstract:
We work with the signed digit representation of abstract real numbers, which roughly is the binary representation enriched by the additional digit -1. The main objective of this paper is an algorithm which takes a sequence of signed digit representations of reals and returns the signed digit representation of their limit, if the sequence converges. As a first application we use this algorithm toge…
▽ More
We work with the signed digit representation of abstract real numbers, which roughly is the binary representation enriched by the additional digit -1. The main objective of this paper is an algorithm which takes a sequence of signed digit representations of reals and returns the signed digit representation of their limit, if the sequence converges. As a first application we use this algorithm together with Heron's method to build up an algorithm which converts the signed digit representation of a non-negative real number into the signed digit representation of its square root. Instead of writing the algorithms first and proving their correctness afterwards, we work the other way round, in the tradition of program extraction from proofs. In fact we first give constructive proofs, and from these proofs we then compute the extracted terms, which is the desired algorithm. The correctness of the extracted term follows directly by the Soundness Theorem of program extraction. In order to get the extracted term from some proofs which are often quite long, we use the proof assistant Minlog. However, to apply the extracted terms, the programming language Haskell is useful. Therefore after each proof we show a notation of the extracted term, which can be easily rewritten as a definition in Haskell.
△ Less
Submitted 25 March, 2025; v1 submitted 27 July, 2018;
originally announced July 2018.
