To: seminaire@pauillac.inria.fr From: Bruno.Barras@inria.fr Subject: SEM - INRIA : LogiCal - 27/04/01 - Paris - FR Vous pouvez maintenant vous abonner à nos annonces de séminaires http://pauillac.inria.fr/seminaires/subscribe.html S E M I N A I R E . ___ / _ _ / _ / / / \ / \ / / __| / |___ |_/ |_/ / |__ |_/ |_ ___ . / / ___ __ /_ _ / _/ /| /| _ __ __ _ _ / / / /_ / __| / / |/ | / \ /_ / / \ | / __| |___ / / __/ |_ |_/ |_ / | |_/__/ |_ |_/ |/ |_/ I N R I A - Rocquencourt Salle de conference du Bat 11 Vendredi 27 avril, 10h30 ------------------------------------------------ Martijn Oostdijk (joint work with Olga Caprotti) ------------------------------------------------ ===================================== How to prove Prime(1234567891) in Coq ===================================== In this talk we present how proof assistants (PA) and computer algebra systems (CAS) can be combined in order to get efficient yet formal proofs. We give a (skeptical) formalization of Pocklington's Criterion in the PA Coq. This criterion states that to prove primality of a number, it is sufficient to find a number of witnesses that satisfy certain algebraic equalities. Finding those witnesses is a computationally intensive task, best performed by a CAS. Therefore, we combine Coq to a CAS using the OpenMath language. The formalization of the criterion in Coq is interesting because we are forced to prove a large amount of trivial and less trivial results which are usually not explicitly mentioned in the informal proof. The application to generate primality proofs demonstrates that combining PAs and CASs is feasible and can be very helpful. It also helps us understand the limitations of a PA with respect to computations. If time (and technology) permits, there will be a short system demo.