Statistics on digital libraries of mathematics (2009)
Abstract. We present statistics on the standard libraries of four major
Deduction using the ProofWeb system (2009)
Cezary Kaliszyk, Femke Van Raamsdonk, Freek Wiedijk, Maxim Hendriks, Roel De Vrijer
This is the manual of the ProofWeb system that was implemented at the Radboud University Nijmegen and the Free University Amsterdam in the SURF education innovation project Web deduction for...
Formal Proof—Getting Started (2009)
Today highly nontrivial mathematics is routinely being encoded in the computer, ensuring a reliability that is orders of a magnitude larger than if one had just used human minds. Such an encoding is...
The µ-inverse for the HOL Light reals (2008)
We present an alternative definition of the multiplicative inverse for the real numbers as formalized in John Harrison’s HOL Light system. 1 Defining the real numbers The two common ways to define...
LFM 2004 Preliminary Version A logical framework with explicit conversions Abstract (2008)
The type theory λP corresponds to the logical framework LF. In this paper we present λH, a variant of λP where convertibility is not implemented by means of the customary conversion rule, but...
We use filters of open sets to provide a semantics justifying formally the use of infinity in informal limit calculations in calculus, and in the same kind of calculations in computer algebra. We...
Teaching logic using a state-of-the-art (2008)
Cezary Kaliszyk, Freek Wiedijk, Maxim Hendriks, Femke Raamsdonk
proof assistant
The formal proof sketch challenge (2008)
Abstract. A formal proof sketch is a way to present a formal proof in a style that is close to an informal proof, but which also is a skeleton of the full formal proof (this makes it easy to relate...
Summary. A Pythagorean triple is a set of positive integers {a,b,c} with a 2 + b 2 = c 2. We prove that every Pythagorean triple is of the form a = n 2 − m 2 b = 2mn c = n 2 + m 2 or is a multiple...
1. SQUARE ROOTS OF PRIMES ARE IRRATIONAL (2008)
Summary. We prove the irrationality of square roots of prime numbers and of the number e. In order to be able to prove the last, a proof is given that number e = exp(1) as defined in the Mizar...
C-CoRN, the Constructive Coq Repository at (2008)
Luís Cruz-filipe, Herman Geuvers, Freek Wiedijk
Nijmegen. It consists of a library of constructive algebra and analysis, formalized in the theorem prover Coq. In this paper we explain the structure, the contents and the use of the library....
Chains on a Grating in Euclidean Space 1 (2008)
We follow the rules: X, x, y, z are sets and n, m, k, k ′ , d ′ are natural numbers. We now state two propositions: (1) For all real numbers x, y such that x < y there exists a real number z...
We use filters of open sets to provide a semantics justifying the use of infinity in informal limit calculations in calculus, and in the same kind of calculations in computer algebra. We compare the...
Abstract. We estimate the cost of formalizing a proper standard library for proof checking of mathematics in the spirit of the QED project. Apparently it will take approximately 140 man-years. This...
Summary. A Pythagorean triple is a set of positive integers {a,b,c} with a 2 + b 2 = c 2. We prove that every Pythagorean triple is of the form a = n 2 − m 2 b = 2mn c = n 2 + m 2 or is a multiple...
The QED manifesto revisited (2008)
Abstract. We present an overview of the current state of formalization of mathematics, and argue what will be needed to make the vision from the QED manifesto come true. This short and intentionally...
Certified Computer Algebra on top of an Interactive Theorem Prover (2008)
Cezary Kaliszyk, Freek Wiedijk
1 Introduction Computer algebra systems do not always give correct answers. This happensbecause those systems do not certify the operations performed. There can be various reasons for errors in a...
C-CoRN, the Constructive Coq Repository at (2008)
Abstract. We present C-CoRN, the Constructive Coq Repository at Nijmegen. It consists of a library of constructive algebra and analysis, formalized in the theorem prover Coq. In this paper we explain...
LFM 2004 Preliminary Version A logical framework with explicit conversions Abstract (2008)
The type theory λP corresponds to the logical framework LF. In this paper we present λH, a variant of λP where convertibility is not implemented by means of the customary conversion rule, but...
Institute for Computing and Information Sciences, (2008)
Cezary Kaliszyk, Freek Wiedijk
Abstract. We present a prototype of a computer algebra system that is built on top of a proof assistant, HOL Light. This architecture guarantees that one can be certain that the system will make no...
1. SQUARE ROOTS OF PRIMES ARE IRRATIONAL (2008)
Summary. We prove the irrationality of square roots of prime numbers and of the number e. In order to be able to prove the last, a proof is given that number e = exp(1) as defined in the Mizar...
Equational Reasoning in Algebraic Structures: a Complete Tactic (2008)
Luís Cruz-filipe, Freek Wiedijk
We present rational, a Coq tactic for equational reasoning in abelian groups, commutative rings, and fields. We give an mathematical description of the method that this tactic uses, which abstracts...
Conditional Computing (what proof checking needs from computer algebra) (2008)
We show that current computer algebra systems are not suitable for use in proof checking, because they don’t answer the right kind of question. By analyzing the calculations from a sample...
A proposed syntax for binders in Mizar (2008)
Abstract. Binders like ‘lim ’ (for limits), ‘ � ’ (for summation) and ‘ � ’ (for integration) are an essential part of the language of mathematics. They are the ‘higher order ’...
Encoding the HOL Light logic in Coq (2008)
Abstract. We show how to encode the HOL Light logic in Coq. This makes an automatic translation of HOL proofs to Coq possible. The translated HOL proofs refer to translated HOL data types but those...
The Mathematical Vernacular (2008)
A ‘mathematical vernacular ’ is a formal language for writing mathematical proofs which resembles the natural language from mathematical texts. Several systems (Hyperproof, Mizar, Isabelle/Isar)...
Herman Geuvers, Y Pollack, Freek Wiedijk
We describe a framework of algebraic structures in the proof assistant Coq. We have developed this framework as part of the FTA project in Nijmegen, in which a constructive proof of the Fundamental...
Chains on a Grating in Euclidean Space 1 (2008)
We follow the rules: X, x, y, z are sets and n, m, k, k ′ , d ′ are natural numbers. We now state two propositions: (1) For all real numbers x, y such that x < y there exists a real number z...
The meaning of infinity in calculus and (2008)
computer algebra systems
C-CoRN, the Constructive Coq Repository at Nijmegen (2008)
Luís Cruz-filipe, Herman Geuvers, Freek Wiedijk
We present C-CoRN, the Constructive Coq Repository at Nijmegen. It consists of a mathematical library of constructive algebra and analysis formalized in the theorem prover Coq. We explain the...
The QED manifesto revisited (2008)
Abstract. We present an overview of the current state of formalization of mathematics, and argue what will be needed to make the vision from the QED manifesto come true. This short and intentionally...
MMode A Mizar Mode for the proof assistant Coq (2008)
Abstract. We present a set of tactics for version 7.4 of the Coq proof assistant which makes it possible to write proofs for Coq in a language similar to the proof language of the Mizar system. These...
Mizar’s Soft Type System (2008)
Abstract. In Mizar, unlike in most other proof assistants, the types are not part of the foundations of the system. Mizar is based on untyped set theory, which means that in Mizar expressions are...
A new implementation of Automath (2008)
Abstract. This paper presents aut, a modern Automath checker. It is a straightforward re-implementation of the Zandleven Automath checker from the seventies. It was implemented about five years ago,...
Teaching logic using a state-of-the-art (2008)
Cezary Kaliszyk, Freek Wiedijk, Maxim Hendriks, Femke Raamsdonk
proof assistant
Skeleton for the Proof development leading to the Fundamental Theorem of Algebra (2007)
Herman Geuvers Randy, Y Pollack, Freek Wiedijk, Jan Zwanenburg
13.97> if its negation is the equality, i.e. :(a # b) $ a = b for all a; b. Fact 1.2 The negation of an apartness relation on S is an equivalence relation on S which is stable, i.e. :::(a # b) !...
Persistence in Algebraic Specifications Persistence in Algebraic Specifications (2007)
Freek Wiedijk, Academisch Proefschrift, Door Frederik Wiedijk
ter verkrijging van de graad van doctor aan de Universiteit van Amsterdam, op gezag van de Rector Magnificus prof. dr. P.W.M. de Meijer, in het openbaar te verdedigen in de Aula der Universiteit...
Examples of erroneous specifications (2007)
Freek Wiedijk, Academisch Proefschrift, Frederik Wiedijk
ter verkrijging van de graad van doctor aan de Universiteit van Amsterdam, op gezag van de Rector Magnificus prof. dr. P.W.M. de Meijer, in het openbaar te verdedigen in de Aula der Universiteit...
A Rigorous Theory of Innite Limits (2007)
We give rigorous denitions and theorems supporting the use of symbols for (various kinds of) innity and undenedness in calculations involving limits. Such calculations are often made on paper and...
We present an alternative denition of the multiplicative inverse for the real numbers as formalized in John Harrison's HOL Light system. 1 Dening the real numbers The two common ways to dene the...
Abstract. We study de Bruijn's `loss factor ' between the size of an ordinary mathematical exposition and its full formal translation inside a computer. This factor is determined by a...
Skeleton for the Proof development leading to the Fundamental Theorem of Algebra (2007)
Herman Geuvers, Y Pollack, Freek Wiedijk, Jan Zwanenburg
A basic ingredient of constructive real numbers is the apartness relation #. This is a constructive version of the (classical) inequality on reals: two real numbers are apart if it can positively be...
Conditional Computing (what proof checking needs from computer algebra) (2007)
We show that current computer algebra systems are not suitable for use in proof checking, because they don't answer the right kind of question. By analyzing the calculations from a sample...
The Mathematical Vernacular (2007)
A `mathematical vernacular ' is a formal language for writing mathematical proofs which resembles the natural language from mathematical texts. Several systems (Hyperproof, Mizar, Isabelle/Isar)...
Abstract. We estimate the cost of formalizing a proper standard library for proof checking of mathematics in the spirit of the QED project. Apparently it will take approximately 140 man-years. This...
The Formal Proof Sketch Challenge (2007)
A formal proof sketch is a way to present a formal proof in a style that is close to an informal proof, but which also is a skeleton of the full formal proof (this makes it easy to relate the...
The Meaning Of Infinity In Calculus And Computer Algebra Systems (2007)
We use lters of open sets to provide a semantics justifying the use of in nity in informal limit calculations in calculus, and in the same kind of calculations in computer algebra. We compare the...
A new implementation of Automath (2007)
This paper presents aut, a modern Automath checker. It is a straight-forward re-implementation of the Zandleven Automath checker from the seventies. It was implemented about five years ago, in the...
Encoding the HOL Light logic in Coq (2007)
We show how to encode the HOL Light logic in Coq. This makes an automatic translation of HOL proofs to Coq possible. The translated HOL proofs refer to translated HOL data types but those data types...
A Constructive Algebraic Hierarchy in Coq (2007)
Herman Geuvers, Y Pollack, Freek Wiedijk
We describe a framework of algebraic structures in the proof assistant Coq. We have developed this framework as part of the FTA project in Nijmegen, in which a constructive proof of the Fundamental...
C-CoRN, the Constructive Coq Repository at Nijmegan (2007)
We present C-CoRN, the Constructive Coq Repository at Nijmegen. It consists of a library of constructive algebra and analysis, formalized in the theorem prover Coq. In this paper we explain the...
The QED Manifesto Revisited (2007)
We present an overview of the current state of formalization of mathematics, and argue what will be needed to make the vision from the QED manifesto come true.
Herman Geuvers, Milad Niqui, Bas Spitters, Freek Wiedijk
In the present paper, we will discuss various aspects of computable/constructive analysis, namely semantics, proofs and computations. We will present some of the problems and solutions of exact real...
Herman Geuvers, Milad Niqui, Bas Spitters, Freek Wiedijk
In the present paper, we will discuss various aspects of computable/constructive analysis, namely semantics, proofs and computations. We will present some of the problems and solutions of exact real...
Herman Geuvers, Milad Niqui, Bas Spitters, Freek Wiedijk
In the present paper, we will discuss various aspects of computable/constructive analysis, namely semantics, proofs and computations. We will present some of the problems and solutions of exact real...
The challenge of computer mathematics (2005)
Henk Barendregt, Freek Wiedijk
Progress in the foundations of mathematics has made it possible to formulate all thinkable mathematical concepts, algorithms and proofs in one language and in an impeccable way. This is not in spite...
The challenge of computer mathematics (2005)
Henk Barendregt, Freek Wiedijk
Progress in the foundations of mathematics has made it possible to formulate all thinkable mathematical concepts, algorithms and proofs in one language and in an impeccable way. This is not in spite...
The challenge of computer mathematics (2005)
Henk Barendregt, Freek Wiedijk
Progress in the foundations of mathematics has made it possible to formulate all thinkable mathematical concepts, algorithms and proofs in one language and in an impeccable way. This is not in spite...
Hierarchical Reflection (2004)
Luís Cruz-filipe, Freek Wiedijk
Abstract. The technique of reflection is a way to automate proof construction in type theoretical proof assistants. Reflection is based on the definition of a type of syntactic expressions that gets...
Abstract. Formalized mathematics currently does not look much like informal mathematics. Also, formalizing mathematics currently seems far too much work to be worth the time of the working...
Hierarchical Reflection (2004)
Luís Cruz-filipe, Freek Wiedijk
Abstract. The technique of reflection is a way to automate proof construction in type theoretical proof assistants. Reflection is based on the definition of a type of syntactic expressions that gets...
Abstract. We define the notion of formal proof sketch for the mathematical language Mizar. We show by examples that formal proof sketches are very close to informal mathematical proofs. We discuss...
MMode, a Mizar Mode for the proof assistant Coq (2003)
M. Giero, F. Wiedijk, Mariusz Giero, Freek Wiedijk
We present a set of tactics for version 7.4 of the Coq proof assistant which makes it possible to write proofs for Coq in a language similar to the proof language of the Mizar system. These tactics...
Comparing mathematical provers (2003)
Abstract. We compare fifteen systems for the formalizations of mathematics with the computer. We present several tables that list various properties of these programs. The three main dimensions on...
Comparing Mathematical Provers (2003)
We compare fteen systems for the formalizations of mathematics with the computer. We present several tables that list various properties of these programs. The three main dimensions on which we...
The algebraic hierarchy of the FTA Project (2002)
Herman Geuvers, Y Pollack, Freek Wiedijk, Jan Zwanenburg
Abstract. We describe a framework for algebraic expressions for the proof assistant Coq. This framework has been developed as part of the FTA project in Nijmegen, in which a complete proof of the...
Abstract. The correctness of proofs is increasingly being veried with computer programs called `proof checkers'. Examples of such proof checkers are Mizar, ACL2, PVS, Nuprl, HOL, Isabelle and...
The algebraic hierarchy of the FTA Project (2002)
Herman Geuvers, Y Pollack, Freek Wiedijk, Jan Zwanenburg
Abstract. We describe a framework for algebraic expressions for the proof assistant Coq. This framework has been developed as part of the FTA project in Nijmegen, in which a complete proof of the...
We de ne the notion of formal proof sketch for the mathematical language Mizar. We show by examples that formal proof sketches are very close to informal mathematical proofs. We discuss some ways in...
A Comparison of the Mathematical Proof Languages Mizar and Isar (2002)
The mathematical proof checker Mizar by Andrzej Trybulec uses a proof input language that is much more readable than the input languages of most other proof assistants. This system also di#ers in...
Abstract. This paper addresses the crucial issue in the design of a proof development system of how to deal with partial functions and the related question of how to treat undefined terms. Often the...
A Comparison of Mizar and Isar (2002)
Abstract. The mathematical proof checker Mizar by Andrzej Trybulec uses a proof input language that is much more readable than the input languages of most other proof assistants. This system also...
The Fifteen Provers of the World (2002)
Informal Henk Barendregt, Theorema Markus Rosenkranz, Tudor Jebelean, Armin Fiedler, Martin Pollet, Freek Wiedijk
We compare the styles of several proof assistants for mathematics. We present Pythagoras' proof of the irrationality of 2 both informal and formalized in (1) HOL, (2) Mizar, (3) PVS, (4) Coq,...
A comparison of Mizar and Isar (2002)
The mathematical proof checker Mizar by Andrzej Trybulec uses a proof input language that is much more readable than the input languages of most other proof assistants. This system also diers in many...
A constructive proof of the Fundamental Theorem of Algebra without using the rationals (2001)
Herman Geuvers, Freek Wiedijk, Jan Zwanenburg
Abstract. In the FTA project in Nijmegen we have formalized a constructive proof of the Fundamental Theorem of Algebra. In the formalization, we have rst dened the (constructive) algebraic hierarchy...
Mizar light for HOL light (2001)
Abstract. There are two dierent approaches to formalizing proofs in a computer: the procedural approach (which is the one of the HOL system) and the declarative approach (which is the one of the...
A constructive proof of the Fundamental Theorem of Algebra without using the rationals (2001)
Herman Geuvers, Freek Wiedijk, Jan Zwanenburg
Abstract. In the FTA project in Nijmegen we have formalized a constructive proof of the Fundamental Theorem of Algebra. In the formalization, we have first defined the (constructive) algebraic...
Mizar light for HOL light (2001)
Abstract. There are two different approaches to formalizing proofs in a computer: the procedural approach (which is the one of the HOL system) and the declarative approach (which is the one of the...
Skeleton for the Proof development leading to the Fundamental Theorem of Algebra (2000)
Herman Geuvers, Randy Pollack, Y Pollack, Freek Wiedijk, Jan Zwanenburg
13.97> if its negation is the equality, i.e. :(a # b) $ a = b for all a; b. Fact 1.2 The negation of an apartness relation on S is an equivalence relation on S which is stable, i.e. :::(a # b) !...
A Rigorous Theory of Infinite Limits (2000)
We give rigorous definitions and theorems supporting the use of symbols for (various kinds of) infinity and undefinedness in calculations involving limits. Such calculations are often made on paper...
Abstract. We study de Bruijn’s ‘loss factor ’ between the size of an ordinary mathematical exposition and its full formal translation inside a computer. This factor is determined by a...
Skeleton for the Proof development leading to the Fundamental Theorem of Algebra (2000)
Herman Geuvers, Y Pollack, Freek Wiedijk, Jan Zwanenburg
Definition 1.1 A binary relation # on a set S is an apartness relation if
This note presents an introduction to the Mizar system, followed by a brief comparison between Mizar and Coq. Appended are a Mizar grammar and an annotated example of a complete Mizar article. 1 What...
This note presents an introduction to the Mizar system, followed by a brief comparison between Mizar and Coq. Appended are a Mizar grammar and an annotated example of a complete Mizar article. 1 What...