Abstract

Co-authors: Guillaume Melquiond (Inria, Université Paris-Saclay), Thomas Sibut-Pinote (Inria, Université Paris-Saclay; École polytechnique) Finding an elementary form for an antiderivative is often a difficult task, thus numerical integration is a common tool when it comes to making sense of a definite integral. Some of the numerical integration methods can even be made rigorous: not only do they compute an approximation of the integral value but they also bound its inaccuracy. Yet numerical integration is still missing from the toolbox when performing formal proofs in analysis, but also in other areas of mathematics that shall involve the evaluation of some integrals like number theory, dynamical systems… In this talk, we describe and discuss an efficient method for automatically computing and proving bounds on some definite integrals inside the Coq proof assistant.