Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation

DOI10.1007/s10817-017-9444-2zbMath1448.68455OpenAlexW2780997459WikidataQ113901245 ScholiaQ113901245MaRDI QIDQ1663216

Yves Bertot, Laurent Théry, Laurence Rideau

Publication date: 21 August 2018

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-017-9444-2

zbMATH Keywords

Coq proof assistantPIarithmetic geometric meansBailey-Borwein-Plouffe formulaBBPformal proofs in real analysis

Mathematics Subject Classification ID

Evaluation of number-theoretic constants (11Y60) Numerical approximation and computational geometry (primarily algorithms) (65D99) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (2)

What is the point of computers? A question for pure mathematicians ⋮ Quantitative continuity and Computable Analysis in Coq

Uses Software

• Coq
• Isabelle/HOL
• MPFR
• Why3
• Mizar
• HOL Light
• Flocq
• WhyML
• Coquelicot
• GitHub
• kepler98

Cites Work

• Unnamed Item
• Unnamed Item
• Proving tight bounds on univariate expressions with elementary functions in Coq
• Isabelle/HOL. A proof assistant for higher-order logic
• A proof of GMP square root
• Coquelicot: a user-friendly library of real analysis for Coq
• Fast multiplication of large numbers
• A Refinement-Based Approach to Computational Algebra in Coq
• Refinements for Free!
• On the rapid computation of various polylogarithmic constants
• Certified Exact Transcendental Real Number Computation in Coq
• MPFR
• Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
• A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers
• Fast Multiple-Precision Evaluation of Elementary Functions
• Computation of π Using Arithmetic-Geometric Mean
• Type classes for efficient exact real arithmetic in Coq
• Views of Pi: definition and computation
• Why3 — Where Programs Meet Provers
• Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
• Extending Coq with Imperative Features and Its Application to SAT Verification

This page was built for publication: Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation