scholarly journals Formalization of real analysis: a survey of proof assistants and libraries

2015 ◽  
Vol 26 (7) ◽  
pp. 1196-1233 ◽  
Author(s):  
SYLVIE BOLDO ◽  
CATHERINE LELAY ◽  
GUILLAUME MELQUIOND
Keyword(s):  
Real Analysis ◽  
Proof Assistants ◽  
Real Numbers ◽  
Similar Role ◽  
Proof Systems ◽  
Hol Light

In the recent years, numerous proof systems have improved enough to be used for formally verifying non-trivial mathematical results. They, however, have different purposes and it is not always easy to choose which one is adapted to undertake a formalization effort. In this survey, we focus on properties related to real analysis: real numbers, arithmetic operators, limits, differentiability, integrability and so on. We have chosen to look into the formalizations provided in standard by the following systems: Coq, HOL4, HOL Light, Isabelle/HOL, Mizar, ProofPower-HOL, and PVS. We have also accounted for large developments that play a similar role or extend standard libraries: ACL2(r) for ACL2, C-CoRN/MathClasses for Coq, and the NASA PVS library. This survey presents how real numbers have been defined in these various provers and how the notions of real analysis described above have been formalized. We also look at the methods of automation these systems provide for real analysis.

Sets and Numbers

2021 ◽  
pp. 3-27
Author(s):  
James Davidson
Keyword(s):  
Set Theory ◽  
Real Line ◽  
Euclidean Distance ◽  
Final Section ◽  
Real Analysis ◽  
Real Numbers ◽  
The Real ◽  
Basic Ideas ◽  
Distance Sets

This chapter covers set theory. The topics include set algebra, relations, orderings and mappings, countability and sequences, real numbers, sequences and limits, and set classes including monotone classes, rings, fields, and sigma fields. The final section introduces the basic ideas of real analysis including Euclidean distance, sets of the real line, coverings, and compactness.

scholarly journals Extensional constructive real analysis via locators

2020 ◽  
pp. 1-25
Author(s):  
Auke B. Booij
Keyword(s):  
Cauchy Sequence ◽  
Computable Analysis ◽  
Real Analysis ◽  
Additional Structure ◽  
Real Numbers ◽  
Decimal Expansion ◽  
Discrete Information

Abstract Real numbers do not admit an extensional procedure for observing discrete information, such as the first digit of its decimal expansion, because every extensional, computable map from the reals to the integers is constant, as is well known. We overcome this by considering real numbers equipped with additional structure, which we call a locator. With this structure, it is possible, for instance, to construct a signed-digit representation or a Cauchy sequence, and conversely, these intensional representations give rise to a locator. Although the constructions are reminiscent of computable analysis, instead of working with a notion of computability, we simply work constructively to extract observable information, and instead of working with representations, we consider a certain locatedness structure on real numbers.

scholarly journals A monadic, functional implementation of real numbers

2007 ◽  
Vol 17 (1) ◽  
pp. 129-159 ◽  
Author(s):  
RUSSELL ÓCONNOR
Keyword(s):  
Real Number ◽  
Large Scale ◽  
Metric Spaces ◽  
Continuous Functions ◽  
Proof Assistants ◽  
Elementary Functions ◽  
Real Numbers ◽  
Mathematical Proofs ◽  
Regular Functions ◽  
Regular Sequences

Large scale real number computation is an essential ingredient in several modern mathematical proofs. Because such lengthy computations cannot be verified by hand, some mathematicians want to use software proof assistants to verify the correctness of these proofs. This paper develops a new implementation of the constructive real numbers and elementary functions for such proofs by using the monad properties of the completion operation on metric spaces. Bishop and Bridges's notion (Bishop and Bridges 1985) of regular sequences is generalised to what I call regular functions, which form the completion of any metric space. Using the monad operations, continuous functions on length spaces (which are a common subclass of metric spaces) are created by lifting continuous functions on the original space. A prototype Haskell implementation has been created. I believe that this approach yields a real number library that is reasonably efficient for computation, and still simple enough to verify its correctness easily.

scholarly journals A FORMAL PROOF OF THE KEPLER CONJECTURE

2017 ◽  
Vol 5 ◽  
Author(s):  
THOMAS HALES ◽  
MARK ADAMS ◽  
GERTRUD BAUER ◽  
TAT DAT DANG ◽  
JOHN HARRISON ◽  
...  
Keyword(s):  
Formal Proof ◽  
Proof Assistants ◽  
Sphere Packings ◽  
Kepler Conjecture ◽  
Hol Light ◽  
Published Account

This article describes a formal proof of the Kepler conjecture on dense sphere packings in a combination of the HOL Light and Isabelle proof assistants. This paper constitutes the official published account of the now completed Flyspeck project.

scholarly journals FREGE’S CONSTRAINT AND THE NATURE OF FREGE’S FOUNDATIONAL PROGRAM

2018 ◽  
Vol 12 (1) ◽  
pp. 97-143 ◽  
Author(s):  
MARCO PANZA ◽  
ANDREA SERENI
Keyword(s):  
Mathematical Theory ◽  
Essential Elements ◽  
Real Analysis ◽  
Natural Numbers ◽  
Real Numbers ◽  
Crispin Wright ◽  
Definition Of ◽  
Image Position ◽  
Shed Light

AbstractRecent discussions on Fregean and neo-Fregean foundations for arithmetic and real analysis pay much attention to what is called either ‘Application Constraint’ ($AC$) or ‘Frege Constraint’ ($FC$), the requirement that a mathematical theory be so outlined that it immediately allows explaining for its applicability. We distinguish between two constraints, which we, respectively, denote by the latter of these two names, by showing how$AC$generalizes Frege’s views while$FC$comes closer to his original conceptions. Different authors diverge on the interpretation of$FC$and on whether it applies to definitions of both natural and real numbers. Our aim is to trace the origins of$FC$and to explore how different understandings of it can be faithful to Frege’s views about such definitions and to his foundational program. After rehearsing the essential elements of the relevant debate (§1), we appropriately distinguish$AC$from$FC$(§2). We discuss six rationales which may motivate the adoption of different instances of$AC$and$FC$(§3). We turn to the possible interpretations of$FC$(§4), and advance a Semantic$FC$(§4.1), arguing that while it suits Frege’s definition of natural numbers (4.1.1), it cannot reasonably be imposed on definitions of real numbers (§4.1.2), for reasons only partly similar to those offered by Crispin Wright (§4.1.3). We then rehearse a recent exchange between Bob Hale and Vadim Batitzky to shed light on Frege’s conception of real numbers and magnitudes (§4.2). We argue that an Architectonic version of$FC$is indeed faithful to Frege’s definition of real numbers, and compatible with his views on natural ones. Finally, we consider how attributing different instances of$FC$to Frege and appreciating the role of the Architectonic$FC$can provide a more perspicuous understanding of his foundational program, by questioning common pictures of his logicism (§5).

scholarly journals Gauge Integral

2017 ◽  
Vol 25 (3) ◽  
pp. 217-225
Author(s):  
Roland Coghetto
Keyword(s):  
Real Interval ◽  
Proof Assistants ◽  
Lebesgue Integral ◽  
Riemann Integral ◽  
Hol Light ◽  
Mizar Mathematical Library ◽  
System 1

Summary Some authors have formalized the integral in the Mizar Mathematical Library (MML). The first article in a series on the Darboux/Riemann integral was written by Noboru Endou and Artur Korniłowicz: [6]. The Lebesgue integral was formalized a little later [13] and recently the integral of Riemann-Stieltjes was introduced in the MML by Keiko Narita, Kazuhisa Nakasho and Yasunari Shidama [12]. A presentation of definitions of integrals in other proof assistants or proof checkers (ACL2, COQ, Isabelle/HOL, HOL4, HOL Light, PVS, ProofPower) may be found in [10] and [4]. Using the Mizar system [1], we define the Gauge integral (Henstock-Kurzweil) of a real-valued function on a real interval [a, b] (see [2], [3], [15], [14], [11]). In the next section we formalize that the Henstock-Kurzweil integral is linear. In the last section, we verified that a real-valued bounded integrable (in sense Darboux/Riemann [6, 7, 8]) function over a interval a, b is Gauge integrable. Note that, in accordance with the possibilities of the MML [9], we reuse a large part of demonstrations already present in another article. Instead of rewriting the proof already contained in [7] (MML Version: 5.42.1290), we slightly modified this article in order to use directly the expected results.

The combinatorics of the splitting theorem

1997 ◽  
Vol 62 (1) ◽  
pp. 197-224
Author(s):  
Kyriakos Kontostathis
Keyword(s):  
Complexity Theory ◽  
Product Space ◽  
Recursion Theory ◽  
Inner Product ◽  
Real Analysis ◽  
Real Numbers ◽  
Stage Of Development ◽  
Priority Method ◽  
The Subject ◽  
Made In

The complexity of priority proofs in recursion theory has been growing since the first priority proofs in [1] and [11]. Refined versions of classic priority proofs can be found in [18]. To this date, this part of recursion theory is at about the same stage of development as real analysis was in the early days, when the notions of topology, continuity, compactness, vector space, inner product space, etc., were not invented. There were no general theorems involving these concepts to prove results about the real numbers and the proofs were repetitive and lengthy.The priority method contains an unprecedent wealth of combinatorics which is used to answer questions in recursion theory and is bound to have applications in many other fields as well. Unfortunately, very little progress has been made in finding theorems to formulate the combinatorial part of the priority method so as to answer questions without having to reprove the combinatorics in each case.Lempp and Lerman in [10] provide an overview of the subject. The entire edifice of definitions and theorems which formulate the combinatorics of the priority method has acquired the name Priority Theory. From a different vein, Groszek and Slaman in [2] have initiated a program to classify priority constructions in terms of how much induction or collection is needed to carry them out. This program studies the complexity of priority proofs and can be called Complexity Theory of Priority Proofs or simply Complexity.

scholarly journals Experiences from Exporting Major Proof Assistant Libraries

2021 ◽  
Author(s):  
Michael Kohlhase ◽  
Florian Rabe
Keyword(s):  
Theorem Proving ◽  
Proof Assistant ◽  
Proof Assistants ◽  
Social Challenges ◽  
Future System ◽  
Hol Light ◽  
System Interoperability

AbstractThe interoperability of proof assistants and the integration of their libraries is a highly valued but elusive goal in the field of theorem proving. As a preparatory step, in previous work, we translated the libraries of multiple proof assistants, specifically the ones of Coq, HOL Light, IMPS, Isabelle, Mizar, and PVS into a universal format: OMDoc/MMT. Each translation presented great theoretical, technical, and social challenges, some universal and some system-specific, some solvable and some still open. In this paper, we survey these challenges and compare and evaluate the solutions we chose. We believe similar library translations will be an essential part of any future system interoperability solution, and our experiences will prove valuable to others undertaking such efforts.

Sign in / Sign up

Export Citation Format

Share Document