Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation
type: Item
instance of: scholarly article
title: Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation
zbMATH Open document ID: 1448.68455
author: Yves Bertot
author: Laurence Rideau
author: Laurent Théry
published in: Journal of Automated Reasoning
publication date: 2018-08-21T00:00:00Z
Mathematics Subject Classification ID: 68V15
Mathematics Subject Classification ID: 11Y60
Mathematics Subject Classification ID: 65D99
zbMATH DE Number: 6921412
zbMATH Keywords: formal proofs in real analysis
zbMATH Keywords: Coq proof assistant
zbMATH Keywords: arithmetic geometric means
zbMATH Keywords: Bailey-Borwein-Plouffe formula
zbMATH Keywords: BBP
zbMATH Keywords: PI
describes a project that uses: Why3
describes a project that uses: MPFR
describes a project that uses: Mizar
describes a project that uses: WhyML
describes a project that uses: kepler98
describes a project that uses: Coquelicot
describes a project that uses: Coq
describes a project that uses: Flocq
describes a project that uses: Isabelle/HOL
describes a project that uses: HOL Light
describes a project that uses: GitHub
MaRDI profile type: Publication
full work available at URL: s10817-017-9444-2
OpenAlex ID: W2780997459
cites work: Extending Coq with Imperative Features and Its Application to SAT Verification
cites work: On the rapid computation of various polylogarithmic constants
cites work: Views of Pi: definition and computation
cites work: A proof of GMP square root
cites work: Computation of π Using Arithmetic-Geometric Mean
cites work: Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
cites work: Coquelicot: a user-friendly library of real analysis for Coq
cites work: Q3751634
cites work: Fast Multiple-Precision Evaluation of Elementary Functions
cites work: Refinements for Free!
cites work: A Refinement-Based Approach to Computational Algebra in Coq
cites work: Why3 — Where Programs Meet Provers
cites work: MPFR
cites work: A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers
cites work: Q4231030
cites work: Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
cites work: Type classes for efficient exact real arithmetic in Coq
cites work: Proving tight bounds on univariate expressions with elementary functions in Coq
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: Certified Exact Transcendental Real Number Computation in Coq
cites work: Fast multiplication of large numbers
Wikidata QID: Q113901245
DOI: 10.1007/S10817-017-9444-2
description: scientific article; zbMATH DE number 6921412