A Matter of Trust: Skeptical Communication Between Coq and External Provers

Most theorem provers are either hard to trust because they are large programs or hard to use due to a lack of automation. They are thus used by two different communities depending on the property one needs most: the ability to prove quickly a large amount of theorems or a high level of safety. My thesis studies a communication between these different kinds of tools, by asking for proof witnesses in addition to yes/no answers from automated provers, and checking them in safe provers. It offers both a way to safely combine proofs coming from all these provers in order to benefit from the advantages of all of them and guaranties to automated theorem provers