Decimals of Pi: An example in verified programming about mathematics

Title: Decimals of Pi: An example in verified programming about mathematics
Speaker: Yves Bertot (INRIA)
Time: 15:00, Thursday, July 26th, 2012
Venue: Room 337, 3rd Floor, Building 5#, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences
Abstract: What is the definition of Pi?  There are several possible ways to give this definition: the surface of a circle, as computed by Riemann Integrals; the first positive root of the cosinus function, where cosinus is given by a power series; or four times the limit of the series “1 – 1/3 + 1/5 + … +(-1)^i/(2 * i + 1) + …”.

In this talk, I study the mathematical proofs relating two such definitions, I provide a program that computes arbitrary close rational approximations of Pi,  and I show that all these mathematical facts can be verified using a
formal verification tool, the Coq system.  This example helps showing how proof verification tools can now help understanding advanced mathematics and what are the remaining difficulties for this objective.

Bio:
Yves Bertot has been a researcher at Inria since 1992, after obtaining a PhD at University of Nice under the supervision of Gilles Kahn.  He studied programming environments for programming languages (the Centaur system), proof systems (the Coq system), the formal verification of compilers, proofs in algorithmic geometry, proofs about infinite streams and real numbers. With P. Castéran, he is the author of a book on program verification using
the Coq system.