Quels sont les modes concrets d’élaboration des démonstrations en logique ? Cet article tente d’apporter des éléments de réponses à cette question en analysant un processus récent de développement et d’implémentation d’un logiciel de démonstration de théorèmes par des chercheurs en logique et en intelligence artificielle. L’étude de ce cas montre comment la production de démonstrations logiques peut relever d’une forte activité expérimentale et d’un important travail d’observation, par-delà une opposition canonique effectuée entre sciences déductives et sciences expérimentales.