Investigations in Computer-Aided Mathematics : Experimentation, Computation, and Certification. (Investigations en Mathématiques Assistées par Ordinateur : Expérimentation, Calcul et Certification).

This thesis presents three contributions to the topic of computer-assisted proofs: both in the case of proofs relying on computations and of formal proofs produced and verified using a piece of software called a proof assistant. We first illustrate the theme of experimentation at the service of proofs by programming a symbolic manipulation tool and using it to find and demonstrate a result about matrix multiplications. In a second part, we use a proof assistant to write a proof of Apéry’s theorem, which is based on complex computations. These computations are performed by an efficient external program and are then verified by this proof software. In the third contribution, we propose a program which computes integrals and simultaneously builds proof that the result is correct. We use this program to find errors in published results. Université Paris-Saclay Espace Technologique / Immeuble Discovery Route de l’Orme aux Merisiers RD 128 / 91190 Saint-Aubin, France 1