# Views of pi: definition and computation

Yves Bertot, Guillaume Allais

Research output: Contribution to journalArticle

### Abstract

We study several formal proofs and algorithms related to the number pi in the context of Coq's standard library.  In particular, we clarify the relation between roots of the cosine function and the limit of the alternated series whose terms are the inverse of odd natural numbers (known as Leibnitz' formula).We give a formal description of the arctangent function and its expansion as a power series.  We then study other possible descriptions of pi, first as the surface of the unit disk, second as the limit of perimeters of regular polygons with an increasing number of sides.In a third section, we concentrate on techniques to effectively compute approximations of pi in the proof assistant by relying on rational numbers and decimal representations.
Language English 105-129 25 Journal of Formalized Reasoning 7 1 10.6092/issn.1972-5787/4343 Published - 2014

Pi
Regular polygon
Formal Proof
Odd number
Perimeter
Natural number
Power series
Unit Disk
Roots
Series
Term
Approximation

### Keywords

• Archimedes
• arctangent
• Coq
• Gregory's formula
• pi

### Cite this

@article{8c707e1115f1460c9a1c64a0f5fca6e9,
title = "Views of pi: definition and computation",
abstract = "We study several formal proofs and algorithms related to the number pi in the context of Coq's standard library.  In particular, we clarify the relation between roots of the cosine function and the limit of the alternated series whose terms are the inverse of odd natural numbers (known as Leibnitz' formula).We give a formal description of the arctangent function and its expansion as a power series.  We then study other possible descriptions of pi, first as the surface of the unit disk, second as the limit of perimeters of regular polygons with an increasing number of sides.In a third section, we concentrate on techniques to effectively compute approximations of pi in the proof assistant by relying on rational numbers and decimal representations.",
keywords = "Archimedes, arctangent, Coq, Gregory's formula, pi",
author = "Yves Bertot and Guillaume Allais",
year = "2014",
doi = "10.6092/issn.1972-5787/4343",
language = "English",
volume = "7",
pages = "105--129",
journal = "Journal of Formalized Reasoning",
issn = "1972-5787",
number = "1",

}

Views of pi : definition and computation. / Bertot, Yves; Allais, Guillaume.

In: Journal of Formalized Reasoning, Vol. 7, No. 1, 2014, p. 105-129.

Research output: Contribution to journalArticle

TY - JOUR

T1 - Views of pi

T2 - Journal of Formalized Reasoning

AU - Bertot, Yves

AU - Allais, Guillaume

PY - 2014

Y1 - 2014

N2 - We study several formal proofs and algorithms related to the number pi in the context of Coq's standard library.  In particular, we clarify the relation between roots of the cosine function and the limit of the alternated series whose terms are the inverse of odd natural numbers (known as Leibnitz' formula).We give a formal description of the arctangent function and its expansion as a power series.  We then study other possible descriptions of pi, first as the surface of the unit disk, second as the limit of perimeters of regular polygons with an increasing number of sides.In a third section, we concentrate on techniques to effectively compute approximations of pi in the proof assistant by relying on rational numbers and decimal representations.

AB - We study several formal proofs and algorithms related to the number pi in the context of Coq's standard library.  In particular, we clarify the relation between roots of the cosine function and the limit of the alternated series whose terms are the inverse of odd natural numbers (known as Leibnitz' formula).We give a formal description of the arctangent function and its expansion as a power series.  We then study other possible descriptions of pi, first as the surface of the unit disk, second as the limit of perimeters of regular polygons with an increasing number of sides.In a third section, we concentrate on techniques to effectively compute approximations of pi in the proof assistant by relying on rational numbers and decimal representations.

KW - Archimedes

KW - arctangent

KW - Coq

KW - Gregory's formula

KW - pi

UR - https://jfr.unibo.it/index

U2 - 10.6092/issn.1972-5787/4343

DO - 10.6092/issn.1972-5787/4343

M3 - Article

VL - 7

SP - 105

EP - 129

JO - Journal of Formalized Reasoning

JF - Journal of Formalized Reasoning

SN - 1972-5787

IS - 1

ER -